diff options
| author | Kazuhiko Sakaguchi | 2020-09-29 15:11:18 +0900 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2020-09-29 17:35:30 +0900 |
| commit | 04fbe5e3bb858f0931cfe0b1d9722a8d872ada50 (patch) | |
| tree | d6a6fab72b34624a197adf20913fcc935d218427 /mathcomp/_CoqProject | |
| parent | 7a34bf388b368b450f20a7e10e5a3076370d2d52 (diff) | |
Generalize interval lemmas
- Generalize `mem0_itv(cc|oo)_xNx` and `oppr_itv(|oo|co|oc|cc)` lemmas from
`numFieldType` to `numDomainType`, which have been specialized in PR #458
accidentally.
- Generalize `mid_in_itv(|oo|cc)` lemmas from `realFieldType` to `numFieldType`.
Diffstat (limited to 'mathcomp/_CoqProject')
0 files changed, 0 insertions, 0 deletions