diff options
| author | Cyril Cohen | 2020-09-29 12:57:16 +0200 |
|---|---|---|
| committer | GitHub | 2020-09-29 12:57:16 +0200 |
| commit | 5fc83c2c7610f7034e5c0e92b18093deb340995d (patch) | |
| tree | d6a6fab72b34624a197adf20913fcc935d218427 | |
| parent | 7a34bf388b368b450f20a7e10e5a3076370d2d52 (diff) | |
| parent | 04fbe5e3bb858f0931cfe0b1d9722a8d872ada50 (diff) | |
Merge pull request #600 from pi8027/mid_in_itv
Generalize some interval lemmas
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 4 | ||||
| -rw-r--r-- | mathcomp/algebra/interval.v | 4 |
2 files changed, 6 insertions, 2 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 130b98e..1e9c4eb 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -234,6 +234,10 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). and they respectively mean open and close bounds as right bounds. This change gives us the canonical "left to right" ordering of interval bounds. +- in `interval.v`: + + Lemmas `mid_in_itv(|oo|cc)` have been generalized from `realFieldType` to + `numFieldType`. + ### Renamed - `big_rmcond` -> `big_rmcond_in` (cf Changed section) diff --git a/mathcomp/algebra/interval.v b/mathcomp/algebra/interval.v index d6ea076..067a457 100644 --- a/mathcomp/algebra/interval.v +++ b/mathcomp/algebra/interval.v @@ -582,7 +582,7 @@ Import GRing.Theory Num.Theory. Section IntervalNumDomain. -Variable R : numFieldType. +Variable R : numDomainType. Implicit Types x : R. Lemma mem0_itvcc_xNx x : (0 \in `[- x, x]) = (0 <= x). @@ -614,7 +614,7 @@ End IntervalNumDomain. Section IntervalField. -Variable R : realFieldType. +Variable R : numFieldType. Local Notation mid x y := ((x + y) / 2%:R). |