From fb3b19301cbd5863fdf250876afb0e87a7e41af1 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 26 Jun 2024 12:18:38 +0900 Subject: [PATCH 1/3] new factory for algebra of sets Co-authored-by: @JeremyDubut Co-authored-by: @AkihisaYamada --- CHANGELOG_UNRELEASED.md | 5 +++++ classical/classical_sets.v | 3 +++ theories/measure.v | 22 ++++++++++++++++++++++ theories/topology.v | 10 ++++++++-- 4 files changed, 38 insertions(+), 2 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 542d716f80..f755ae0a88 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/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` diff --git a/classical/classical_sets.v b/classical/classical_sets.v index 90d18a5156..dd371b0a20 100644 --- a/classical/classical_sets.v +++ b/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. diff --git a/theories/measure.v b/theories/measure.v index 00cb507ff9..832837cfc5 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -1189,6 +1189,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 ; diff --git a/theories/topology.v b/theories/topology.v index eb7c846cb6..fafdc65ba6 100644 --- a/theories/topology.v +++ b/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]. @@ -5360,11 +5362,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. @@ -5380,6 +5385,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. From fc5ba13b8ca3a4af8c121b7c5387eeda6cdf19e9 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 9 Jul 2024 23:31:42 +0900 Subject: [PATCH 2/3] symmetric difference Co-authored-by: Takafumi Saikawa --- CHANGELOG_UNRELEASED.md | 11 ++++++- classical/classical_sets.v | 59 ++++++++++++++++++++++++++++++++++++++ theories/measure.v | 41 ++++++++++++++++++++++++-- 3 files changed, 108 insertions(+), 3 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index f755ae0a88..de68f052a9 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -10,7 +10,16 @@ + lemma `setCD` - in `measure.v`: - + factory `isAlgebraOfSetsD` + + factory `isAlgebraOfSets_setD` + +- in `classical_sets.v`: + + definition `sym_diff`, notation ``` `^` ``` + + lemmas `sym_diffxx`, `sym_diff_setU`, `sym_diff_set`, `sym_diff_setI`, + `sym_diffC`, `sym_diffA`, `sym_diff0`, `sym_diffE`, `sym_diffT`, `sym_diffv`, + `sym_diff_def` + +- in `measure.v`: + + factory `isRingOfSets_sym_diff` - in `classical_sets.v`: + lemma `setDU` diff --git a/classical/classical_sets.v b/classical/classical_sets.v index dd371b0a20..ea03a4f09b 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -42,6 +42,7 @@ From mathcomp Require Import mathcomp_extra boolp. (* | `` `\|` `` |==| $\cup$ *) (* | `` `&` `` |==| $\cap$ *) (* | `` `\` `` |==| set difference *) +(* | `` `^` `` |==| symmetric difference *) (* | `` ~` `` |==| set complement *) (* | `` `<=` `` |==| $\subseteq$ *) (* | `` f @` A `` |==| image by f of A *) @@ -244,6 +245,7 @@ Reserved Notation "~` A" (at level 35, right associativity). Reserved Notation "[ 'set' ~ a ]" (at level 0, format "[ 'set' ~ a ]"). Reserved Notation "A `\` B" (at level 50, left associativity). Reserved Notation "A `\ b" (at level 50, left associativity). +Reserved Notation "A `^` B" (at level 52, left associativity). (* Reserved Notation "A `+` B" (at level 54, left associativity). Reserved Notation "A +` B" (at level 54, left associativity). @@ -400,6 +402,10 @@ Notation "A `\` B" := (setD A B) : classical_set_scope. Notation "A `\ a" := (A `\` [set a]) : classical_set_scope. Notation "[ 'disjoint' A & B ]" := (disj_set A B) : classical_set_scope. +Definition sym_diff {T : Type} (A B : set T) := (A `\` B) `|` (B `\` A). +Arguments sym_diff _ _ _ _ /. +Notation "A `^` B" := (sym_diff A B) : classical_set_scope. + Notation "'`I_' n" := [set k | is_true (k < n)%N]. Notation "\bigcup_ ( i 'in' P ) F" := @@ -1117,6 +1123,59 @@ Lemma bigcupM1r T1 T2 (A1 : T2 -> set T1) (A2 : set T2) : \bigcup_(i in A2) (A1 i `*` [set i]) = A1 ``*` A2. Proof. by apply/predeqP => -[i j]; split=> [[? ? [? /= -> //]]|[]]; exists j. Qed. +Lemma sym_diffxx A : A `^` A = set0. +Proof. by rewrite /sym_diff setDv setU0. Qed. + +Lemma sym_diff0 A : A `^` set0 = A. +Proof. by rewrite /sym_diff setD0 set0D setU0. Qed. + +Lemma sym_diffT A : A `^` [set: T] = ~` A. +Proof. by rewrite /sym_diff setDT set0U setTD. Qed. + +Lemma sym_diffv A : A `^` ~` A = [set: T]. +Proof. by rewrite /sym_diff setDE setCK setIid setDE setIid setUv. Qed. + +Lemma sym_diffC A B : A `^` B = B `^` A. +Proof. by rewrite /sym_diff setUC. Qed. + +Lemma sym_diffA A B C : A `^` (B `^` C) = (A `^` B) `^` C. +Proof. +rewrite /sym_diff; apply/seteqP; split => x/=; +by have [|] := pselect (A x); have [|] := pselect (B x); + have [|] := pselect (C x); tauto. +Qed. + +Lemma sym_diff_def A B : A `^` B = (A `&` ~` B) `|` (~` A `&` B). +Proof. by rewrite /sym_diff !setDE (setIC B). Qed. + +Lemma sym_diffE A B : A `^` B = (A `|` B) `\` (A `&` B). +Proof. +rewrite /sym_diff; apply/seteqP; split => x/=; +by have [|] := pselect (A x); have [|] := pselect (B x); tauto. +Qed. + +Lemma sym_diff_setU A B : (A `^` B) `^` (A `&` B) = A `|` B. +Proof. +rewrite /sym_diff; apply/seteqP; split => x/=; +by have [|] := pselect (A x); have [|] := pselect (B x); tauto. +Qed. + +Lemma sym_diff_setD A B : A `^` (A `&` B) = A `\` B. +Proof. by rewrite /sym_diff; apply/seteqP; split => x/=; tauto. Qed. + +Lemma sym_diff_setI A B : (A `|` B) `\` (A `^` B) = A `&` B. +Proof. +rewrite /sym_diff; apply/seteqP; split => x/=; +by have [|] := pselect (A x); have [|] := pselect (B x); tauto. +Qed. + +Lemma setI_sym_diff A B C : A `&` (B `^` C) = (A `&` B) `^` (A `&` C). +Proof. +rewrite /sym_diff; apply/seteqP; split => x/=; +by have [|] := pselect (A x); have [|] := pselect (B x); + have [|] := pselect (C x); tauto. +Qed. + End basic_lemmas. #[global] Hint Resolve subsetUl subsetUr subIsetl subIsetr subDsetl subDsetr : core. diff --git a/theories/measure.v b/theories/measure.v index 832837cfc5..3adaa24576 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -189,6 +189,7 @@ From HB Require Import structures. (* setSD_closed G == the set of sets G is closed under proper *) (* difference *) (* setDI_closed G == the set of sets G is closed under difference *) +(* sym_diff_closed G == the set of sets G is closed by symmetric difference *) (* ndseq_closed G == the set of sets G is closed under non-decreasing *) (* countable union *) (* niseq_closed G == the set of sets G is closed under non-increasing *) @@ -354,6 +355,7 @@ Definition setI_closed := forall A B, G A -> G B -> G (A `&` B). Definition setU_closed := forall A B, G A -> G B -> G (A `|` B). Definition setSD_closed := forall A B, B `<=` A -> G A -> G B -> G (A `\` B). Definition setDI_closed := forall A B, G A -> G B -> G (A `\` B). +Definition sym_diff_closed := forall A B, G A -> G B -> G (A `^` B). Definition fin_bigcap_closed := forall I (D : set I) A_, finite_set D -> (forall i, D i -> G (A_ i)) -> @@ -1164,6 +1166,39 @@ HB.instance Definition _ := SemiRingOfSets_isRingOfSets.Build d T measurableU. HB.end. +HB.factory Record isRingOfSets_sym_diff (d : measure_display) T + of Pointed T := { + measurable : set (set T) ; + measurable_nonempty : measurable !=set0 ; + measurable_sym_diff : sym_diff_closed measurable ; + measurable_setI : setI_closed measurable }. + +HB.builders Context d T of isRingOfSets_sym_diff d T. + +Let m0 : measurable set0. +Proof. +have [A mA] := measurable_nonempty. +have := measurable_sym_diff mA mA. +by rewrite sym_diffxx. +Qed. + +Let mU : setU_closed measurable. +Proof. +move=> A B mA mB; rewrite -sym_diff_setU. +apply: measurable_sym_diff; first exact: measurable_sym_diff. +exact: measurable_setI. +Qed. + +Let mD : setDI_closed measurable. +Proof. +move=> A B mA mB; rewrite -sym_diff_setD. +by apply: measurable_sym_diff => //; exact: measurable_setI. +Qed. + +HB.instance Definition _ := isRingOfSets.Build d T m0 mU mD. + +HB.end. + HB.factory Record isAlgebraOfSets (d : measure_display) T of Pointed T := { measurable : set (set T) ; measurable0 : measurable set0 ; @@ -1189,13 +1224,13 @@ HB.instance Definition _ := RingOfSets_isAlgebraOfSets.Build d T measurableT. HB.end. -HB.factory Record isAlgebraOfSetsD (d : measure_display) T of Pointed T := { +HB.factory Record isAlgebraOfSets_setD (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. +HB.builders Context d T of isAlgebraOfSets_setD d T. Let m0 : measurable set0. Proof. by rewrite -(setDT setT); apply: measurableD; exact: measurableT. Qed. @@ -1209,6 +1244,8 @@ Qed. HB.instance Definition _ := isRingOfSets.Build d T m0 mU measurableD. +HB.instance Definition _ := RingOfSets_isAlgebraOfSets.Build d T measurableT. + HB.end. HB.factory Record isMeasurable (d : measure_display) T of Pointed T := { From 9ef13c280b4ac892dd1276a511efa9611ccb2efa Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 29 Jul 2024 17:01:06 +0900 Subject: [PATCH 3/3] addressing comments --- CHANGELOG_UNRELEASED.md | 11 +++--- classical/classical_sets.v | 79 +++++++++++++++++++++++--------------- theories/measure.v | 24 ++++++------ theories/normedtype.v | 2 +- 4 files changed, 65 insertions(+), 51 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index de68f052a9..c28821c11d 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -13,13 +13,12 @@ + factory `isAlgebraOfSets_setD` - in `classical_sets.v`: - + definition `sym_diff`, notation ``` `^` ``` - + lemmas `sym_diffxx`, `sym_diff_setU`, `sym_diff_set`, `sym_diff_setI`, - `sym_diffC`, `sym_diffA`, `sym_diff0`, `sym_diffE`, `sym_diffT`, `sym_diffv`, - `sym_diff_def` - + + definition `setX`, notation ``` `^` ``` + + lemmas `setX0`, `set0X`, `setXK`, `setXC`, `setXA`, `setIXl`, `mulrXr`, + `setX_def`, `setXE`, `setXU`, `setXI`, `setXD`, `setXCT`, `setCXT`, `setXTC`, `setTXC` + - in `measure.v`: - + factory `isRingOfSets_sym_diff` + + factory `isRingOfSets_setX` - in `classical_sets.v`: + lemma `setDU` diff --git a/classical/classical_sets.v b/classical/classical_sets.v index ea03a4f09b..8a39953d57 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -402,9 +402,9 @@ Notation "A `\` B" := (setD A B) : classical_set_scope. Notation "A `\ a" := (A `\` [set a]) : classical_set_scope. Notation "[ 'disjoint' A & B ]" := (disj_set A B) : classical_set_scope. -Definition sym_diff {T : Type} (A B : set T) := (A `\` B) `|` (B `\` A). -Arguments sym_diff _ _ _ _ /. -Notation "A `^` B" := (sym_diff A B) : classical_set_scope. +Definition setX {T : Type} (A B : set T) := (A `\` B) `|` (B `\` A). +Arguments setX _ _ _ _ /. +Notation "A `^` B" := (setX A B) : classical_set_scope. Notation "'`I_' n" := [set k | is_true (k < n)%N]. @@ -1123,59 +1123,71 @@ Lemma bigcupM1r T1 T2 (A1 : T2 -> set T1) (A2 : set T2) : \bigcup_(i in A2) (A1 i `*` [set i]) = A1 ``*` A2. Proof. by apply/predeqP => -[i j]; split=> [[? ? [? /= -> //]]|[]]; exists j. Qed. -Lemma sym_diffxx A : A `^` A = set0. -Proof. by rewrite /sym_diff setDv setU0. Qed. +Lemma setX0 : right_id set0 (@setX T). +Proof. by move=> A; rewrite /setX setD0 set0D setU0. Qed. -Lemma sym_diff0 A : A `^` set0 = A. -Proof. by rewrite /sym_diff setD0 set0D setU0. Qed. +Lemma set0X : left_id set0 (@setX T). +Proof. by move=> A; rewrite /setX set0D setD0 set0U. Qed. -Lemma sym_diffT A : A `^` [set: T] = ~` A. -Proof. by rewrite /sym_diff setDT set0U setTD. Qed. +Lemma setXK A : A `^` A = set0. +Proof. by rewrite /setX setDv setU0. Qed. -Lemma sym_diffv A : A `^` ~` A = [set: T]. -Proof. by rewrite /sym_diff setDE setCK setIid setDE setIid setUv. Qed. +Lemma setXC : commutative (@setX T). +Proof. by move=> A B; rewrite /setX setUC. Qed. -Lemma sym_diffC A B : A `^` B = B `^` A. -Proof. by rewrite /sym_diff setUC. Qed. +Lemma setXTC A : A `^` [set: T] = ~` A. +Proof. by rewrite /setX setDT set0U setTD. Qed. -Lemma sym_diffA A B C : A `^` (B `^` C) = (A `^` B) `^` C. +Lemma setTXC A : [set: T] `^` A = ~` A. +Proof. by rewrite setXC setXTC. Qed. + +Lemma setXA : associative (@setX T). Proof. -rewrite /sym_diff; apply/seteqP; split => x/=; +move=> A B C; rewrite /setX; apply/seteqP; split => x/=; by have [|] := pselect (A x); have [|] := pselect (B x); have [|] := pselect (C x); tauto. Qed. -Lemma sym_diff_def A B : A `^` B = (A `&` ~` B) `|` (~` A `&` B). -Proof. by rewrite /sym_diff !setDE (setIC B). Qed. - -Lemma sym_diffE A B : A `^` B = (A `|` B) `\` (A `&` B). +Lemma setIXl : left_distributive (@setI T) (@setX T). Proof. -rewrite /sym_diff; apply/seteqP; split => x/=; -by have [|] := pselect (A x); have [|] := pselect (B x); tauto. +move=> A B C; rewrite /setX; apply/seteqP; split => x/=; +by have [|] := pselect (A x); have [|] := pselect (B x); + have [|] := pselect (C x); tauto. Qed. -Lemma sym_diff_setU A B : (A `^` B) `^` (A `&` B) = A `|` B. +Lemma setIXr : right_distributive (@setI T) (@setX T). +Proof. by move=> A B C; rewrite setIC setIXl -2!(setIC A). Qed. + +Lemma setX_def A B : A `^` B = (A `\` B) `|` (B `\` A). +Proof. by []. Qed. + +Lemma setXE A B : A `^` B = (A `|` B) `\` (A `&` B). Proof. -rewrite /sym_diff; apply/seteqP; split => x/=; +rewrite /setX; apply/seteqP; split => x/=; by have [|] := pselect (A x); have [|] := pselect (B x); tauto. Qed. -Lemma sym_diff_setD A B : A `^` (A `&` B) = A `\` B. -Proof. by rewrite /sym_diff; apply/seteqP; split => x/=; tauto. Qed. - -Lemma sym_diff_setI A B : (A `|` B) `\` (A `^` B) = A `&` B. +Lemma setXU A B : (A `^` B) `^` (A `&` B) = A `|` B. Proof. -rewrite /sym_diff; apply/seteqP; split => x/=; +rewrite /setX; apply/seteqP; split => x/=; by have [|] := pselect (A x); have [|] := pselect (B x); tauto. Qed. -Lemma setI_sym_diff A B C : A `&` (B `^` C) = (A `&` B) `^` (A `&` C). +Lemma setXI A B : (A `|` B) `\` (A `^` B) = A `&` B. Proof. -rewrite /sym_diff; apply/seteqP; split => x/=; -by have [|] := pselect (A x); have [|] := pselect (B x); - have [|] := pselect (C x); tauto. +rewrite /setX; apply/seteqP; split => x/=; +by have [|] := pselect (A x); have [|] := pselect (B x); tauto. Qed. +Lemma setXD A B : A `^` (A `&` B) = A `\` B. +Proof. by rewrite /setX; apply/seteqP; split => x/=; tauto. Qed. + +Lemma setXCT A : A `^` ~` A = [set: T]. +Proof. by rewrite /setX setDE setCK setIid setDE setIid setUv. Qed. + +Lemma setCXT A : ~` A `^` A = [set: T]. +Proof. by rewrite setXC setXCT. Qed. + End basic_lemmas. #[global] Hint Resolve subsetUl subsetUr subIsetl subIsetr subDsetl subDsetr : core. @@ -1371,6 +1383,9 @@ HB.instance Definition _ := isMulLaw.Build (set T) set0 setI set0I setI0. HB.instance Definition _ := isAddLaw.Build (set T) setU setI setUIl setUIr. HB.instance Definition _ := isAddLaw.Build (set T) setI setU setIUl setIUr. +HB.instance Definition _ := isComLaw.Build (set T) set0 setX setXA setXC set0X. +HB.instance Definition _ := isAddLaw.Build (set T) setI setX setIXl setIXr. + End SetMonoids. Section base_image_lemmas. diff --git a/theories/measure.v b/theories/measure.v index 3adaa24576..b558468c3a 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -189,7 +189,8 @@ From HB Require Import structures. (* setSD_closed G == the set of sets G is closed under proper *) (* difference *) (* setDI_closed G == the set of sets G is closed under difference *) -(* sym_diff_closed G == the set of sets G is closed by symmetric difference *) +(* setX_closed G == the set of sets G is closed under symmetric *) +(* difference *) (* ndseq_closed G == the set of sets G is closed under non-decreasing *) (* countable union *) (* niseq_closed G == the set of sets G is closed under non-increasing *) @@ -355,7 +356,7 @@ Definition setI_closed := forall A B, G A -> G B -> G (A `&` B). Definition setU_closed := forall A B, G A -> G B -> G (A `|` B). Definition setSD_closed := forall A B, B `<=` A -> G A -> G B -> G (A `\` B). Definition setDI_closed := forall A B, G A -> G B -> G (A `\` B). -Definition sym_diff_closed := forall A B, G A -> G B -> G (A `^` B). +Definition setX_closed := forall A B, G A -> G B -> G (A `^` B). Definition fin_bigcap_closed := forall I (D : set I) A_, finite_set D -> (forall i, D i -> G (A_ i)) -> @@ -1166,33 +1167,32 @@ HB.instance Definition _ := SemiRingOfSets_isRingOfSets.Build d T measurableU. HB.end. -HB.factory Record isRingOfSets_sym_diff (d : measure_display) T +HB.factory Record isRingOfSets_setX (d : measure_display) T of Pointed T := { measurable : set (set T) ; measurable_nonempty : measurable !=set0 ; - measurable_sym_diff : sym_diff_closed measurable ; + measurable_setX : setX_closed measurable ; measurable_setI : setI_closed measurable }. -HB.builders Context d T of isRingOfSets_sym_diff d T. +HB.builders Context d T of isRingOfSets_setX d T. Let m0 : measurable set0. Proof. have [A mA] := measurable_nonempty. -have := measurable_sym_diff mA mA. -by rewrite sym_diffxx. +have := measurable_setX mA mA. +by rewrite setXK. Qed. Let mU : setU_closed measurable. Proof. -move=> A B mA mB; rewrite -sym_diff_setU. -apply: measurable_sym_diff; first exact: measurable_sym_diff. -exact: measurable_setI. +move=> A B mA mB; rewrite -setXU. +by apply: measurable_setX; [exact: measurable_setX|exact: measurable_setI]. Qed. Let mD : setDI_closed measurable. Proof. -move=> A B mA mB; rewrite -sym_diff_setD. -by apply: measurable_sym_diff => //; exact: measurable_setI. +move=> A B mA mB; rewrite -setXD. +by apply: measurable_setX => //; exact: measurable_setI. Qed. HB.instance Definition _ := isRingOfSets.Build d T m0 mU mD. diff --git a/theories/normedtype.v b/theories/normedtype.v index 7215695952..41f16dd137 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -692,7 +692,7 @@ Proof. by rewrite cvgeNyPltr. Qed. Lemma cvgNey f : (\- f @ F --> +oo) <-> (f @ F --> -oo). Proof. rewrite cvgeNyPler cvgeyPger; split=> Foo A Areal; -by near do rewrite -lee_opp2 ?oppeK; apply: Foo; rewrite rpredN. +by near do rewrite -leeN2 ?oppeK; apply: Foo; rewrite rpredN. Unshelve. all: end_near. Qed. Lemma cvgNeNy f : (\- f @ F --> -oo) <-> (f @ F --> +oo).