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 | |
| parent | a65958322cb6ee84f3ebbb68d1fb4867749cf1a0 (diff) | |
another lemma about norm from mathcomp-analysis
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 2 | ||||
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 6 |
2 files changed, 7 insertions, 1 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 957e02c..4de3f44 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -12,7 +12,7 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). - lemmas `ltr_dist_addl`, `ler_dist_addl`, `ltr_distr_addl`, `ler_distr_addl`, `ltr_dist_subl`, `ler_dist_subl`, - `ltr_distr_subr`, `ler_distr_subr` in `ssrnum` + `ltr_distr_subr`, `ler_distr_subr`, `norm_lt_eqF` in `ssrnum` ### Changed 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. |