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

Wrong idea: swap back.

parent 14801d95
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Lebesgue/Set_theory/Set_system/Set_system_def_any.v
+ 1
− 1
View file @ f947d0a2
...@@ -69,7 +69,7 @@ Definition is_Basisf : set (Idx -> set U) := ...@@ -69,7 +69,7 @@ Definition is_Basisf : set (Idx -> set U) :=
fun fB => fun fB =>
(forall i, T (fB i)) /\ (forall i, T (fB i)) /\
(forall A, T A -> (forall A, T A ->
A = unionf_any (fun i => inter (fB i) (prop_cst (incl (fB i) A)))). A = unionf_any (fun i => inter (prop_cst (incl (fB i) A)) (fB i))).
(* FIXME: using (Subset A PB) generates pbs in Set_system_any/is_Basisf_is_Basisp_equiv! *) (* FIXME: using (Subset A PB) generates pbs in Set_system_any/is_Basisf_is_Basisp_equiv! *)
Definition is_Basisp : set_system_class U := Definition is_Basisp : set_system_class U :=
......
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