Skip to content
Snippets Groups Projects
Commit 5dd24100 authored by François Clément's avatar François Clément
Browse files

Renaming sections.

parent 10db5fe4
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 4 additions and 4 deletions
Lebesgue/measurable.v
+ 4
− 4
View file @ 5dd24100
......@@ -303,7 +303,7 @@ Qed.
End measurable_gen_Image_Facts.
Section measurable_gen_Facts2.
Section measurable_gen_Image_Facts2.
Context {E F : Type}. (* Universes. *)
Variable genE : (E -> Prop) -> Prop. (* Generator. *)
......@@ -343,10 +343,10 @@ apply subset_seq_ext.
intros n; rewrite (proj2 (HB n)); easy.
Qed.
End measurable_gen_Facts2.
End measurable_gen_Image_Facts2.
Section measurable_gen_Facts3.
Section measurable_gen_Image_Facts3.
Context {E F : Type}. (* Universes. *)
Variable genE : (E -> Prop) -> Prop. (* Generator. *)
......@@ -367,7 +367,7 @@ apply is_Sigma_algebra_Image.
apply Preimage_Incl_Incl_Image, measurable_gen.
Qed.
End measurable_gen_Facts3.
End measurable_gen_Image_Facts3.
Section measurable_correct.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment