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 /mathcomp | |
| parent | ed3d822bc5a1c3759140b7fd7567f2b4278ae0be (diff) | |
lemma used in mathcomp-analysis
Co-authored-by: Cyril Cohen <cohen@crans.org>
Co-authored-by: Kazuhiko Sakaguchi <pi8027@gmail.com>
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 20 |
1 files changed, 20 insertions, 0 deletions
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. |