diff options
| author | Reynald Affeldt | 2020-06-02 18:14:22 +0900 |
|---|---|---|
| committer | Reynald Affeldt | 2020-06-02 19:53:11 +0900 |
| commit | 3d77e498c075af6f642b3239acf4b18503c1e6bc (patch) | |
| tree | fdad84eda994116eadc8846d77ad738dda2731ff /mathcomp/algebra | |
| parent | a65958322cb6ee84f3ebbb68d1fb4867749cf1a0 (diff) | |
another lemma about norm from mathcomp-analysis
Diffstat (limited to 'mathcomp/algebra')
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index 7a41745..5047868 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -3778,6 +3778,12 @@ Proof. by rewrite distrC => /ltr_dist_subl. Qed. Lemma ler_distr_subr x y e : `|x - y| <= e -> y - e <= x. Proof. by rewrite distrC => /ler_dist_subl. Qed. +Lemma norm_lt_eqF (x y : R) : `|x| < y -> (x == - y = false) * (x == y = false). +Proof. +move=> x1; split; last by rewrite lt_eqF // (le_lt_trans (ler_norm _) x1). +by move: x1; rewrite ltr_norml => /andP[? ?]; rewrite gt_eqF. +Qed. + Lemma exprn_even_ge0 n x : ~~ odd n -> 0 <= x ^+ n. Proof. by move=> even_n; rewrite real_exprn_even_ge0 ?num_real. Qed. |