diff options
| author | Reynald Affeldt | 2020-09-12 17:02:00 +0900 |
|---|---|---|
| committer | Reynald Affeldt | 2020-10-12 09:22:18 +0900 |
| commit | 1cacfb8f5dd8307adbc48b67474055ce455a168d (patch) | |
| tree | 3aed0ee0ed53d01a59359a4797a69b0e3dc06aae | |
| parent | ed3d822bc5a1c3759140b7fd7567f2b4278ae0be (diff) | |
lemma used in mathcomp-analysis
Co-authored-by: Cyril Cohen <cohen@crans.org>
Co-authored-by: Kazuhiko Sakaguchi <pi8027@gmail.com>
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 3 | ||||
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 20 |
2 files changed, 22 insertions, 1 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 22229fe..fe3adce 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -31,7 +31,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). `contraPleq`, `contraPltn`, `contra_not_leq`, `contra_not_ltn`, `contra_leq_not`, `contra_ltn_not` - in `ssralg.v`, new lemma `sumr_const_nat` and `iter_addr_0` - in `ssrnum.v`, new lemma `ler_sum_nat` - +- in `ssrnum.v`, new lemmas `max_real`, `min_real`, `bigmax_real`, `bigmin_real` +` - in `seq.v`, new lemmas: `take_uniq`, `drop_uniq` - in `fintype.v`, new lemmas: `card_geqP`, `card_gt1P`, `card_gt2P`, `card_le1_eqP` (generalizes `fintype_le1P`), diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index 2eefe8e..c28aec2 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -1779,6 +1779,26 @@ move=> hx; rewrite -[X in `|X|]subr0; case: (@real_ltgtP 0 x); by rewrite ?subr0 ?sub0r //; constructor. Qed. +Lemma max_real : {in real &, forall x y, max x y \is real}. +Proof. by move=> x y ? ?; case: real_leP. Qed. + +Lemma min_real : {in real &, forall x y, min x y \is real}. +Proof. by move=> x y ? ?; case: real_leP. Qed. + +Lemma bigmax_real I x0 (r : seq I) (P : pred I) (f : I -> R): + x0 \is real -> {in P, forall t : I, f t \is real} -> + \big[max/x0]_(t <- r | P t) f t \is real. +Proof. +by move=> x0r Pr; elim/big_rec : _ => // i x Pi xr; rewrite max_real ?Pr. +Qed. + +Lemma bigmin_real I x0 (r : seq I) (P : pred I) (f : I -> R): + x0 \is real -> {in P, forall t : I, f t \is real} -> + \big[min/x0]_(t <- r | P t) f t \is real. +Proof. +by move=> x0r Pr; elim/big_rec : _ => // i x Pi xr; rewrite min_real ?Pr. +Qed. + Lemma real_neqr_lt : {in real &, forall x y, (x != y) = (x < y) || (y < x)}. Proof. by move=> * /=; case: real_ltgtP. Qed. |