Merge pull request #314 from math-comp/classical_sets_naming

more uniform variable naming convention
math-comp · Jan 26, 2021 · 31562ae · 31562ae
2 parents 1542c0c + 60271d8
commit 31562ae
Show file tree

Hide file tree

Showing 4 changed files with 470 additions and 433 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -24,6 +24,8 @@
 - in `reals.v`, definition `ceil`, lemmas `RceilE`, `ceil_ge0`, `ceil_le0`
 
 - in `ereal.v`, lemmas `esum_fset_ninfty`, `esum_fset_pinfty`, `esum_pinfty`
+- in `classical_sets.v`, lemmas `setDT`, `set0D`, `setD0`
+- in `classical_sets.v`, lemmas `setC_bigcup`, `setC_bigcap`
 
 - in `measure.v`, definition `sigma_finite`
 
@@ -61,6 +63,7 @@
 
 - in `topology.v`:
   + `ball_le`
+- in `classical_sets.v`, lemma `bigcapCU`
 
 ### Infrastructure