new factory for algebra of sets

Co-authored-by: @JeremyDubut
Co-authored-by: @AkihisaYamada

CHANGELOG_UNRELEASED.md

@@ -6,6 +6,11 @@
 
 - in `topology.v`:
   + lemma `ball_subspace_ball`
+- in `classical_sets.v`:
+  + lemma `setCD`
+
+- in `measure.v`:
+  + factory `isAlgebraOfSetsD`
 
 - in `classical_sets.v`:
   + lemma `setDU`

classical/classical_sets.v

@@ -995,6 +995,9 @@ Qed.
 Lemma setCI A B : ~` (A `&` B) = ~` A `|` ~` B.
 Proof. by rewrite -[in LHS](setCK A) -[in LHS](setCK B) -setCU setCK. Qed.
 
+Lemma setCD A B : ~` (A `\` B) = ~` A `|` B.
+Proof. by rewrite setDE setCI setCK. Qed.
+
 Lemma setDUr A B C : A `\` (B `|` C) = (A `\` B) `&` (A `\` C).
 Proof. by rewrite !setDE setCU setIIr. Qed.
 

theories/measure.v

@@ -1185,6 +1185,28 @@ HB.instance Definition _ := RingOfSets_isAlgebraOfSets.Build d T measurableT.
 
 HB.end.
 
+HB.factory Record isAlgebraOfSetsD (d : measure_display) T of Pointed T := {
+  measurable : set (set T) ;
+  measurableT : measurable [set: T] ;
+  measurableD : setDI_closed measurable
+}.
+
+HB.builders Context d T of isAlgebraOfSetsD d T.
+
+Let m0 : measurable set0.
+Proof. by rewrite -(setDT setT); apply: measurableD; exact: measurableT. Qed.
+
+Let mU : setU_closed measurable.
+Proof.
+move=> A B mA mB.
+rewrite -(setCK A) -setCD -!setTD; apply: measurableD; first exact: measurableT.
+by do 2 apply: measurableD => //; exact: measurableT.
+Qed.
+
+HB.instance Definition _ := isRingOfSets.Build d T m0 mU measurableD.
+
+HB.end.
+
 HB.factory Record isMeasurable (d : measure_display) T of Pointed T := {
   measurable : set (set T) ;
   measurable0 : measurable set0 ;

theories/topology.v

@@ -4772,7 +4772,8 @@ HB.instance Definition _ := Uniform_isPseudoMetric.Build R M
 
 HB.end.
 
-Lemma entourage_ballE {R : numDomainType} {M : pseudoMetricType R} : entourage_ (@ball R M) = entourage.
+Lemma entourage_ballE {R : numDomainType} {M : pseudoMetricType R} :
+  entourage_ (@ball R M) = entourage.
 Proof. by rewrite entourageE_subproof. Qed.
 
 Lemma entourage_from_ballE {R : numDomainType} {M : pseudoMetricType R} :
@@ -4791,7 +4792,8 @@ Definition nbhs_ball_ {R : numDomainType} {T T'} (ball : T -> R -> set T')
 Definition nbhs_ball {R : numDomainType} {M : pseudoMetricType R} :=
   nbhs_ball_ (@ball R M).
 
-Lemma nbhs_ballE {R : numDomainType} {M : pseudoMetricType R} : (@nbhs_ball R M) = nbhs.
+Lemma nbhs_ballE {R : numDomainType} {M : pseudoMetricType R} :
+  @nbhs_ball R M = nbhs.
 Proof.
 rewrite predeq2E => x P; rewrite -nbhs_entourageE; split.
   by move=> [_/posnumP[e] sbxeP]; exists [set xy | ball xy.1 e%:num xy.2].
@@ -5354,11 +5356,14 @@ Qed.
 
 Section pseudoMetric_of_normedDomain.
 Context {K : numDomainType} {R : normedZmodType K}.
+
 Lemma ball_norm_center (x : R) (e : K) : 0 < e -> ball_ Num.norm x e x.
 Proof. by move=> ? /=; rewrite subrr normr0. Qed.
+
 Lemma ball_norm_symmetric (x y : R) (e : K) :
   ball_ Num.norm x e y -> ball_ Num.norm y e x.
 Proof. by rewrite /= distrC. Qed.
+
 Lemma ball_norm_triangle (x y z : R) (e1 e2 : K) :
   ball_ Num.norm x e1 y -> ball_ Num.norm y e2 z -> ball_ Num.norm x (e1 + e2) z.
 Proof.
@@ -5374,6 +5379,7 @@ rewrite /nbhs_ entourage_E predeq2E => x A; split.
   by exists [set xy | ball_ Num.norm xy.1 e xy.2] => //; exists e.
 by move=> [E [e egt0 sbeE] sEA]; exists e => // ??; apply/sEA/sbeE.
 Qed.
+
 End pseudoMetric_of_normedDomain.
 
 HB.instance Definition _ (R : zmodType) := Pointed.on R^o.