proposition: Lemma sedDI_closedP T (G : set (set T)) : setDI_closed G <-> (setI_closed G /\ setD_closed G).
proof: Proof. split=> [GDI|[GI GD]]. by split=> A B => [|AB] => GA GB; rewrite -?setDD//; do ?apply: (GDI). move=> A B GA GB; suff <- : A `\` (A `&` B) = A `\` B. by apply: GD => //; apply: GI. by rewrite setDE setCI setIUr -setDE setDv set0U. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) reals ereal signed topology normedtype sequences esum numfun HB(structures)