diff options
| author | Cyril Cohen | 2021-01-18 16:49:38 +0100 |
|---|---|---|
| committer | GitHub | 2021-01-18 16:49:38 +0100 |
| commit | 35fc6b309a5cc87570255addfd135cb4650ebb43 (patch) | |
| tree | fb83c066a0b3e1b97ec8d62f17ae93d13b74adf2 | |
| parent | 68fab9412b287079164aab5f3eda71fcd65df8cc (diff) | |
| parent | 5e809e16078d4659cd2dbb6c1bbc754fa6d3b6ee (diff) | |
Merge pull request #693 from affeldt-aist/interval_20210114
itv_bound comparison with -oo/+oo
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 2 | ||||
| -rw-r--r-- | mathcomp/algebra/interval.v | 8 |
2 files changed, 10 insertions, 0 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index ad3cae2..1e779c3 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -22,6 +22,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). - in `path.v`, new lemmas: `sorted_pairwise(_in)`, `path_pairwise(_in)`, `cycle_all2rel(_in)`, `pairwise_sort`, and `sort_pairwise_stable`. +- in `interval.v`, new lemmas: `ge_pinftyE`, `le_ninftyE`, `gt_pinfty`, `lt_ninfty`. + ### Changed - In `ssralg.v` and `ssrint.v`, the nullary ring notations `-%R`, `+%R`, `*%R`, diff --git a/mathcomp/algebra/interval.v b/mathcomp/algebra/interval.v index 067a457..4a1cadb 100644 --- a/mathcomp/algebra/interval.v +++ b/mathcomp/algebra/interval.v @@ -217,6 +217,14 @@ Proof. by rewrite /<=%O /= lteifxx. Qed. Lemma bound_ltxx c1 c2 x : (BSide c1 x < BSide c2 x) = (c1 && ~~ c2). Proof. by rewrite /<%O /= lteifxx. Qed. +Lemma ge_pinftyE b : (+oo <= b) = (b == +oo). Proof. by move: b => [|[]]. Qed. + +Lemma le_ninftyE b : (b <= -oo) = (b == -oo). Proof. by case: b => // - []. Qed. + +Lemma gt_pinfty b : (+oo < b) = false. Proof. by []. Qed. + +Lemma lt_ninfty b : (b < -oo) = false. Proof. by case: b => // -[]. Qed. + Definition subitv i1 i2 := let: Interval b1l b1r := i1 in let: Interval b2l b2r := i2 in (b2l <= b1l) && (b1r <= b2r). |