measurable_fun and generated sigma-algebras

math-comp · Sep 6, 2021 · 4080012 · 4080012
1 parent 263862c
commit 4080012
Show file tree

Hide file tree

Showing 2 changed files with 366 additions and 308 deletions.
diff --git a/_CoqProject b/_CoqProject
@@ -22,7 +22,7 @@ theories/normedtype.v
 theories/sequences.v
 theories/cardinality.v
 theories/csum.v
-theories/measure_wip.v
+theories/lebesgue_measure.v
 theories/forms.v
 theories/derive.v
 theories/measure.v