From 589d35a3986647de510299cddfe3716fef3077c3 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 1 Aug 2024 10:14:35 +0900 Subject: [PATCH 1/3] setX -> setY --- CHANGELOG_UNRELEASED.md | 9 ++--- classical/classical_sets.v | 72 +++++++++++++++++++------------------- theories/measure.v | 22 ++++++------ 3 files changed, 52 insertions(+), 51 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index af62a5f2d..a866f6e96 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -13,12 +13,13 @@ + factory `isAlgebraOfSets_setD` - in `classical_sets.v`: - + definition `setX`, notation ``` `^` ``` - + lemmas `setX0`, `set0X`, `setXK`, `setXC`, `setXA`, `setIXl`, `mulrXr`, - `setX_def`, `setXE`, `setXU`, `setXI`, `setXD`, `setXCT`, `setCXT`, `setXTC`, `setTXC` + + definition `setY`, notation ``` `^` ``` + + lemmas `setY0`, `set0Y`, `setYK`, `setYC`, `setYA`, `setIYl`, `mulrYr`, + `setY_def`, `setYE`, `setYU`, `setYI`, `setYD`, `setYCT`, `setCYT`, `setYTC`, `setTYC` - in `measure.v`: - + factory `isRingOfSets_setX` + + defintion `setY_closed` + + factory `isRingOfSets_setY` - in `classical_sets.v`: + lemma `setDU` diff --git a/classical/classical_sets.v b/classical/classical_sets.v index 2afe27710..7756017c4 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 setX {T : Type} (A B : set T) := (A `\` B) `|` (B `\` A). -Arguments setX _ _ _ _ /. -Notation "A `^` B" := (setX A B) : classical_set_scope. +Definition setY {T : Type} (A B : set T) := (A `\` B) `|` (B `\` A). +Arguments setY _ _ _ _ /. +Notation "A `^` B" := (setY A B) : classical_set_scope. Notation "'`I_' n" := [set k | is_true (k < n)%N]. @@ -1123,70 +1123,70 @@ 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 setX0 : right_id set0 (@setX T). -Proof. by move=> A; rewrite /setX setD0 set0D setU0. Qed. +Lemma setY0 : right_id set0 (@setY T). +Proof. by move=> A; rewrite /setY setD0 set0D setU0. Qed. -Lemma set0X : left_id set0 (@setX T). -Proof. by move=> A; rewrite /setX set0D setD0 set0U. Qed. +Lemma set0Y : left_id set0 (@setY T). +Proof. by move=> A; rewrite /setY set0D setD0 set0U. Qed. -Lemma setXK A : A `^` A = set0. -Proof. by rewrite /setX setDv setU0. Qed. +Lemma setYK A : A `^` A = set0. +Proof. by rewrite /setY setDv setU0. Qed. -Lemma setXC : commutative (@setX T). -Proof. by move=> A B; rewrite /setX setUC. Qed. +Lemma setYC : commutative (@setY T). +Proof. by move=> A B; rewrite /setY setUC. Qed. -Lemma setXTC A : A `^` [set: T] = ~` A. -Proof. by rewrite /setX setDT set0U setTD. Qed. +Lemma setYTC A : A `^` [set: T] = ~` A. +Proof. by rewrite /setY setDT set0U setTD. Qed. -Lemma setTXC A : [set: T] `^` A = ~` A. -Proof. by rewrite setXC setXTC. Qed. +Lemma setTYC A : [set: T] `^` A = ~` A. +Proof. by rewrite setYC setYTC. Qed. -Lemma setXA : associative (@setX T). +Lemma setYA : associative (@setY T). Proof. -move=> A B C; rewrite /setX; apply/seteqP; split => x/=; +move=> A B C; rewrite /setY; apply/seteqP; split => x/=; by have [|] := pselect (A x); have [|] := pselect (B x); have [|] := pselect (C x); tauto. Qed. -Lemma setIXl : left_distributive (@setI T) (@setX T). +Lemma setIYl : left_distributive (@setI T) (@setY T). Proof. -move=> A B C; rewrite /setX; apply/seteqP; split => x/=; +move=> A B C; rewrite /setY; apply/seteqP; split => x/=; by have [|] := pselect (A x); have [|] := pselect (B x); have [|] := pselect (C x); tauto. Qed. -Lemma setIXr : right_distributive (@setI T) (@setX T). -Proof. by move=> A B C; rewrite setIC setIXl -2!(setIC A). Qed. +Lemma setIYr : right_distributive (@setI T) (@setY T). +Proof. by move=> A B C; rewrite setIC setIYl -2!(setIC A). Qed. -Lemma setX_def A B : A `^` B = (A `\` B) `|` (B `\` A). +Lemma setY_def A B : A `^` B = (A `\` B) `|` (B `\` A). Proof. by []. Qed. -Lemma setXE A B : A `^` B = (A `|` B) `\` (A `&` B). +Lemma setYE A B : A `^` B = (A `|` B) `\` (A `&` B). Proof. -rewrite /setX; apply/seteqP; split => x/=; +rewrite /setY; apply/seteqP; split => x/=; by have [|] := pselect (A x); have [|] := pselect (B x); tauto. Qed. -Lemma setXU A B : (A `^` B) `^` (A `&` B) = A `|` B. +Lemma setYU A B : (A `^` B) `^` (A `&` B) = A `|` B. Proof. -rewrite /setX; apply/seteqP; split => x/=; +rewrite /setY; apply/seteqP; split => x/=; by have [|] := pselect (A x); have [|] := pselect (B x); tauto. Qed. -Lemma setXI A B : (A `|` B) `\` (A `^` B) = A `&` B. +Lemma setYI A B : (A `|` B) `\` (A `^` B) = A `&` B. Proof. -rewrite /setX; apply/seteqP; split => x/=; +rewrite /setY; 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 setYD A B : A `^` (A `&` B) = A `\` B. +Proof. by rewrite /setY; 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 setYCT A : A `^` ~` A = [set: T]. +Proof. by rewrite /setY setDE setCK setIid setDE setIid setUv. Qed. -Lemma setCXT A : ~` A `^` A = [set: T]. -Proof. by rewrite setXC setXCT. Qed. +Lemma setCYT A : ~` A `^` A = [set: T]. +Proof. by rewrite setYC setYCT. Qed. End basic_lemmas. #[global] @@ -1388,8 +1388,8 @@ 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. +HB.instance Definition _ := isComLaw.Build (set T) set0 setY setYA setYC set0Y. +HB.instance Definition _ := isAddLaw.Build (set T) setI setY setIYl setIYr. End SetMonoids. diff --git a/theories/measure.v b/theories/measure.v index f1e4c9a49..cb4789ba5 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -191,7 +191,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 *) -(* setX_closed G == the set of sets G is closed under symmetric *) +(* setY_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 *) @@ -358,7 +358,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 setX_closed := forall A B, G A -> G B -> G (A `^` B). +Definition setY_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)) -> @@ -1169,32 +1169,32 @@ HB.instance Definition _ := SemiRingOfSets_isRingOfSets.Build d T measurableU. HB.end. -HB.factory Record isRingOfSets_setX (d : measure_display) T +HB.factory Record isRingOfSets_setY (d : measure_display) T of Pointed T := { measurable : set (set T) ; measurable_nonempty : measurable !=set0 ; - measurable_setX : setX_closed measurable ; + measurable_setY : setY_closed measurable ; measurable_setI : setI_closed measurable }. -HB.builders Context d T of isRingOfSets_setX d T. +HB.builders Context d T of isRingOfSets_setY d T. Let m0 : measurable set0. Proof. have [A mA] := measurable_nonempty. -have := measurable_setX mA mA. -by rewrite setXK. +have := measurable_setY mA mA. +by rewrite setYK. Qed. Let mU : setU_closed measurable. Proof. -move=> A B mA mB; rewrite -setXU. -by apply: measurable_setX; [exact: measurable_setX|exact: measurable_setI]. +move=> A B mA mB; rewrite -setYU. +by apply: measurable_setY; [exact: measurable_setY|exact: measurable_setI]. Qed. Let mD : setDI_closed measurable. Proof. -move=> A B mA mB; rewrite -setXD. -by apply: measurable_setX => //; exact: measurable_setI. +move=> A B mA mB; rewrite -setYD. +by apply: measurable_setY => //; exact: measurable_setI. Qed. HB.instance Definition _ := isRingOfSets.Build d T m0 mU mD. From 87940c81d7c0861a9498da1f31dc733f1ef64fbf Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 1 Aug 2024 11:13:13 +0900 Subject: [PATCH 2/3] setM -> setX --- CHANGELOG_UNRELEASED.md | 42 +++++++++++++ classical/cardinality.v | 73 +++++++++++++-------- classical/classical_sets.v | 119 ++++++++++++++++++++++++----------- classical/fsbigop.v | 4 +- theories/esum.v | 4 +- theories/function_spaces.v | 2 +- theories/kernel.v | 12 ++-- theories/lebesgue_integral.v | 52 +++++++-------- theories/measure.v | 26 ++++---- theories/normedtype.v | 2 +- theories/topology.v | 16 ++--- 11 files changed, 233 insertions(+), 119 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index a866f6e96..56dbfebac 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -212,6 +212,48 @@ + `ereal_inf_lb` -> `ereal_inf_lbound` + `ereal_sup_ub` -> `ereal_sup_ubound` +- in `classical_sets.v`: + + `setM` -> `setX` + + `in_setM` -> `in_setX` + + `setMR` -> `setXR` + + `setML` -> `setXL` + + `setM0` -> `setX0` + + `set0M` -> `set0X` + + `setMTT` -> `setXTT` + + `setMT` -> `setXT` + + `setTM` -> `setTX` + + `setMI` -> `setXI` + + `setM_bigcupr` -> `setX_bigcupr` + + `setM_bigcupl` -> `setX_bigcupl` + + `bigcup_setM_dep` -> `bigcup_setX_dep` + + `bigcup_setM` -> `bigcup_setX` + + `fst_setM` -> `fst_setX` + + `snd_setM` -> `snd_setX` + + `in_xsectionM` -> `in_xsectionX` + + `in_ysectionM` -> `in_ysectionX` + + `notin_xsectionM` -> `notin_xsectionX` + + `notin_ysectionM` -> `notin_ysectionX` + + `setSM` -> `setSX` + + `bigcupM1l` -> `bigcupX1l` + + `bigcupM1r` -> `bigcupX1r` + +- in `cardinality.v`: + + `countableMR` -> `countableXR` + + `countableM` -> `countableX` + + `countableML` -> `countableXL` + + `infiniteMRl` -> `infiniteXRl` + + `cardMR_eq_nat` -> `cardXR_eq_nat` + + `finite_setM` -> `finite_setX` + + `finite_setMR` -> `finite_setXR` + + `finite_setML` -> `finite_setXL` + + `fset_setM` -> `fset_setX` + +- in `topology.v`: + + `compact_setM` -> `compact_setX` + +- in `measure.v`: + + `measurableM` -> `measurableX` + ### Generalized - in `constructive_ereal.v`: diff --git a/classical/cardinality.v b/classical/cardinality.v index a9a5f0456..a17e8eb49 100644 --- a/classical/cardinality.v +++ b/classical/cardinality.v @@ -687,7 +687,7 @@ Proof. by move=> ?; apply: finite_setI; left. Qed. Lemma finite_setIr T (A B : set T) : finite_set B -> finite_set (A `&` B). Proof. by move=> ?; apply: finite_setI; right. Qed. -Lemma finite_setM T T' (A : set T) (B : set T') : +Lemma finite_setX T T' (A : set T) (B : set T') : finite_set A -> finite_set B -> finite_set (A `*` B). Proof. elim/Pchoice: T => T in A *; elim/Pchoice: T' => T' in B *. @@ -695,15 +695,18 @@ move=> /finite_fsetP[{}A ->] /finite_fsetP[{}B ->]. apply/finite_fsetP; exists (A `*` B)%fset; apply/predeqP => x. by split; rewrite /= inE => /andP. Qed. +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to finite_setX.")] +Notation finite_setM := finite_setX (only parsing). -Lemma finite_image2 [aT bT rT : Type] [A : set aT] [B : set bT] (f : aT -> bT -> rT) : - finite_set A -> finite_set B -> finite_set [set f x y | x in A & y in B]%classic. -Proof. by move=> fA fB; rewrite image2E; apply/finite_image/finite_setM. Qed. +Lemma finite_image2 [aT bT rT : Type] [A : set aT] [B : set bT] + (f : aT -> bT -> rT) : + finite_set A -> finite_set B -> finite_set [set f x y | x in A & y in B]. +Proof. by move=> fA fB; rewrite image2E; exact/finite_image/finite_setX. Qed. Lemma finite_image11 [xT aT bT rT : Type] [X : set xT] (g : aT -> bT -> rT) (fa : xT -> aT) (fb : xT -> bT) : finite_set (fa @` X) -> finite_set (fb @` X) -> - finite_set [set g (fa x) (fb x) | x in X]%classic. + finite_set [set g (fa x) (fb x) | x in X]. Proof. move=> /(finite_image2 g) /[apply]; apply: sub_finite_set; rewrite image2E. by move=> r/= [x Xx <-]; exists (fa x, fb x) => //; split; exists x. @@ -784,15 +787,17 @@ Lemma fset_setD1 {T : choiceType} (x : T) (A : set T) : finite_set A -> fset_set (A `\ x) = (fset_set A `\ x)%fset. Proof. by move=> fA; rewrite fset_setD// fset_set1. Qed. -Lemma fset_setM {T1 T2 : choiceType} (A : set T1) (B : set T2) : +Lemma fset_setX {T1 T2 : choiceType} (A : set T1) (B : set T2) : finite_set A -> finite_set B -> fset_set (A `*` B) = (fset_set A `*` fset_set B)%fset. Proof. -move=> Afin Bfin; have ABfin : finite_set (A `*` B) by apply: finite_setM. +move=> Afin Bfin; have ABfin : finite_set (A `*` B) by exact: finite_setX. apply/fsetP => i; apply/idP/idP; rewrite !(inE, in_fset_set)//=. by move=> [/mem_set-> /mem_set->]. by move=> /andP[]; rewrite !inE. Qed. +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to fset_setX.")] +Notation fset_setM := fset_setX (only parsing). Definition fst_fset (T1 T2 : choiceType) (A : {fset (T1 * T2)}) : {fset T1} := [fset x.1 | x in A]%fset. @@ -850,19 +855,23 @@ rewrite (@trivIset_bigsetUI _ xpredT)// ?fset_set0//. by rewrite [X in trivIset X F](_ : _ = [set: nat])//; exact/seteqP. Qed. -Lemma finite_setMR (T T' : choiceType) (A : set T) (B : T -> set T') : +Lemma finite_setXR (T T' : choiceType) (A : set T) (B : T -> set T') : finite_set A -> (forall x, A x -> finite_set (B x)) -> finite_set (A `*`` B). Proof. -move=> Afin Bfin; rewrite -bigcupM1l. -by apply: bigcup_finite => // i Ai; apply/finite_setM/Bfin. +move=> Afin Bfin; rewrite -bigcupX1l. +by apply: bigcup_finite => // i Ai; exact/finite_setX/Bfin. Qed. +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to finite_setXR.")] +Notation finite_setMR := finite_setXR (only parsing). -Lemma finite_setML (T T' : choiceType) (A : T' -> set T) (B : set T') : +Lemma finite_setXL (T T' : choiceType) (A : T' -> set T) (B : set T') : (forall x, B x -> finite_set (A x)) -> finite_set B -> finite_set (A ``*` B). Proof. -move=> Afin Bfin; rewrite -bigcupM1r. -by apply: bigcup_finite => // i Ai; apply/finite_setM=> //; apply: Afin. +move=> Afin Bfin; rewrite -bigcupX1r. +by apply: bigcup_finite => // i Ai; apply/finite_setX => //; exact: Afin. Qed. +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to finite_setXL.")] +Notation finite_setML := finite_setXL (only parsing). Lemma fset_set_II n : fset_set `I_n = [fset val i | i in 'I_n]%fset. Proof. @@ -1134,44 +1143,54 @@ apply/pcard_geP/surjPex; exists (fun (k : {i & G i}) => val (projT2 k)). by move=> x [i _] Gix/=; exists (Tagged G (SigSub (mem_set Gix))). Qed. -Lemma countableMR T T' (A : set T) (B : T -> set T') : +Lemma countableXR T T' (A : set T) (B : T -> set T') : countable A -> (forall i, A i -> countable (B i)) -> countable (A `*`` B). Proof. -elim/Ppointed: T => T in A B *; first by rewrite emptyE -bigcupM1l bigcup_set0. +elim/Ppointed: T => T in A B *; first by rewrite emptyE -bigcupX1l bigcup_set0. elim/Ppointed: T' => T' in B *. - by rewrite -bigcupM1l bigcup0// => i; rewrite emptyE setM0. -move=> Ac Bc; rewrite -bigcupM1l bigcup_countable// => i Ai. + by rewrite -bigcupX1l bigcup0// => i; rewrite emptyE setX0. +move=> Ac Bc; rewrite -bigcupX1l bigcup_countable// => i Ai. have /ppcard_leP[f] := Bc i Ai; apply/pcard_geP/surjPex. exists (fun k => (i, f^-1%FUN k)) => -[_ j]/= [-> dj]. by exists (f j) => //=; rewrite funK ?inE. Qed. +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to countableXR.")] +Notation countableMR := countableXR (only parsing). -Lemma countableM T1 T2 (D1 : set T1) (D2 : set T2) : +Lemma countableX T1 T2 (D1 : set T1) (D2 : set T2) : countable D1 -> countable D2 -> countable (D1 `*` D2). -Proof. by move=> D1c D2c; apply: countableMR (fun _ _ => D2c). Qed. +Proof. by move=> D1c D2c; exact: countableXR (fun _ _ => D2c). Qed. +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to countableX.")] +Notation countableM := countableX (only parsing). -Lemma countableML T T' (A : T' -> set T) (B : set T') : +Lemma countableXL T T' (A : T' -> set T) (B : set T') : countable B -> (forall i, B i -> countable (A i)) -> countable (A ``*` B). Proof. -move=> Bc Ac; rewrite -bigcupM1r; apply: bigcup_countable => // i Bi. -by apply: countableM => //; apply: Ac. +move=> Bc Ac; rewrite -bigcupX1r; apply: bigcup_countable => // i Bi. +by apply: countableX => //; exact: Ac. Qed. +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to countableXL.")] +Notation countableML := countableXL (only parsing). -Lemma infiniteMRl T T' (A : set T) (B : T -> set T') : +Lemma infiniteXRl T T' (A : set T) (B : T -> set T') : infinite_set A -> (forall i, B i !=set0) -> infinite_set (A `*`` B). Proof. move=> /infiniteP/pcard_geP[f] /(_ _)/cid-/all_sig[b Bb]. apply/infiniteP/pcard_geP/surjPex; exists (fun x => f x.1). -by move=> i iT; have [a Aa fa] := 'oinvP_f iT; exists (a, b a) => /=. +by move=> i iT; have [a Aa fa] := 'oinvP_f iT; exists (a, b a). Qed. +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to infiniteXRl.")] +Notation infiniteMRl := infiniteXRl (only parsing). -Lemma cardMR_eq_nat T T' (A : set T) (B : T -> set T') : +Lemma cardXR_eq_nat T T' (A : set T) (B : T -> set T') : (A #= [set: nat] -> (forall i, countable (B i) /\ B i !=set0) -> A `*`` B #= [set: nat])%card. Proof. rewrite !card_eq_le => /andP[Acnt /infiniteP Ainfty] /all_and2[Bcnt Bn0]. -by rewrite [(_ #<= _)%card]countableMR//=; apply/infiniteP/infiniteMRl. +by rewrite [(_ #<= _)%card]countableXR//=; exact/infiniteP/infiniteXRl. Qed. +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to cardXR_eq_nat.")] +Notation cardMR_eq_nat := cardXR_eq_nat (only parsing). Lemma eq_cardSP {T : Type} (A : set T) n : reflect (exists2 x, A x & A `\ x #= `I_n) (A #= `I_n.+1). @@ -1194,7 +1213,7 @@ Proof. move=> Dcnt; elim: n => [|n]. rewrite [X in countable X]( _ : _ = [set set0])// eqEsubset II0. by split=> A /=; [rewrite card_eq0; case=> _ /eqP | move->; split]. -move=> /(countableM Dcnt); apply: sub_countable. +move=> /(countableX Dcnt); apply: sub_countable. apply: card_le_trans (card_image_le (fun u => u.1 |` u.2) _). apply: subset_card_le => B [BD] /eq_cardSP [x Bx BDx]. exists (x, B `\ x) => /=; last by apply: setDUK => ? ->. diff --git a/classical/classical_sets.v b/classical/classical_sets.v index 7756017c4..bd448d3fd 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -340,12 +340,12 @@ Definition setU A B := [set x | A x \/ B x]. Definition nonempty A := exists a, A a. Definition setC A := [set a | ~ A a]. Definition setD A B := [set x | A x /\ ~ B x]. -Definition setM T1 T2 (A1 : set T1) (A2 : set T2) := [set z | A1 z.1 /\ A2 z.2]. +Definition setX T1 T2 (A1 : set T1) (A2 : set T2) := [set z | A1 z.1 /\ A2 z.2]. Definition fst_set T1 T2 (A : set (T1 * T2)) := [set x | exists y, A (x, y)]. Definition snd_set T1 T2 (A : set (T1 * T2)) := [set y | exists x, A (x, y)]. -Definition setMR T1 T2 (A1 : set T1) (A2 : T1 -> set T2) := +Definition setXR T1 T2 (A1 : set T1) (A2 : T1 -> set T2) := [set z | A1 z.1 /\ A2 z.1 z.2]. -Definition setML T1 T2 (A1 : T2 -> set T1) (A2 : set T2) := +Definition setXL T1 T2 (A1 : T2 -> set T1) (A2 : set T2) := [set z | A1 z.2 z.1 /\ A2 z.2]. Lemma mksetE (P : T -> Prop) x : [set x | P x] x = P x. @@ -375,9 +375,15 @@ Arguments setI _ _ _ _ /. Arguments setU _ _ _ _ /. Arguments setC _ _ _ /. Arguments setD _ _ _ _ /. -Arguments setM _ _ _ _ _ /. -Arguments setMR _ _ _ _ _ /. -Arguments setML _ _ _ _ _ /. +Arguments setX _ _ _ _ _ /. +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to setX.")] +Notation setM := setX (only parsing). +Arguments setXR _ _ _ _ _ /. +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to setXR.")] +Notation setMR := setXR (only parsing). +Arguments setXL _ _ _ _ _ /. +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to setXL.")] +Notation setML := setXL (only parsing). Arguments fst_set _ _ _ _ /. Arguments snd_set _ _ _ _ /. Arguments subsetP {T A B}. @@ -391,11 +397,11 @@ Notation "a |` A" := ([set a] `|` A) : classical_set_scope. Notation "[ 'set' a1 ; a2 ; .. ; an ]" := (setU .. (a1 |` [set a2]) .. [set an]) : classical_set_scope. Notation "A `&` B" := (setI A B) : classical_set_scope. -Notation "A `*` B" := (setM A B) : classical_set_scope. +Notation "A `*` B" := (setX A B) : classical_set_scope. Notation "A .`1" := (fst_set A) : classical_set_scope. Notation "A .`2" := (snd_set A) : classical_set_scope. -Notation "A `*`` B" := (setMR A B) : classical_set_scope. -Notation "A ``*` B" := (setML A B) : classical_set_scope. +Notation "A `*`` B" := (setXR A B) : classical_set_scope. +Notation "A ``*` B" := (setXL A B) : classical_set_scope. Notation "~` A" := (setC A) : classical_set_scope. Notation "[ 'set' ~ a ]" := (~` [set a]) : classical_set_scope. Notation "A `\` B" := (setD A B) : classical_set_scope. @@ -552,7 +558,7 @@ Proof. by apply/idP/andP; rewrite !inE notin_setE. Qed. Lemma in_setU (x : T) A B : (x \in A `|` B) = (x \in A) || (x \in B). Proof. by apply/idP/orP; rewrite !inE. Qed. -Lemma in_setM T' (x : T * T') A E : (x \in A `*` E) = (x.1 \in A) && (x.2 \in E). +Lemma in_setX T' (x : T * T') A E : (x \in A `*` E) = (x.1 \in A) && (x.2 \in E). Proof. by apply/idP/andP; rewrite !inE. Qed. Lemma set_valP {A} (x : A) : A (val x). @@ -1078,48 +1084,48 @@ apply/seteqP; split=> [x [[Ax|Bx] Cx]|x [[Ax]|[Bx] Cx]]. - by split=> //; right. Qed. -Lemma setM0 T' (A : set T) : A `*` set0 = set0 :> set (T * T'). +Lemma setX0 T' (A : set T) : A `*` set0 = set0 :> set (T * T'). Proof. by rewrite predeqE => -[t u]; split => // -[]. Qed. -Lemma set0M T' (A : set T') : set0 `*` A = set0 :> set (T * T'). +Lemma set0X T' (A : set T') : set0 `*` A = set0 :> set (T * T'). Proof. by rewrite predeqE => -[t u]; split => // -[]. Qed. -Lemma setMTT T' : setT `*` setT = setT :> set (T * T'). +Lemma setXTT T' : setT `*` setT = setT :> set (T * T'). Proof. exact/predeqP. Qed. -Lemma setMT T1 T2 (A : set T1) : A `*` @setT T2 = fst @^-1` A. +Lemma setXT T1 T2 (A : set T1) : A `*` @setT T2 = fst @^-1` A. Proof. by rewrite predeqE => -[x y]; split => //= -[]. Qed. -Lemma setTM T1 T2 (B : set T2) : @setT T1 `*` B = snd @^-1` B. +Lemma setTX T1 T2 (B : set T2) : @setT T1 `*` B = snd @^-1` B. Proof. by rewrite predeqE => -[x y]; split => //= -[]. Qed. -Lemma setMI T1 T2 (X1 : set T1) (X2 : set T2) (Y1 : set T1) (Y2 : set T2) : +Lemma setXI T1 T2 (X1 : set T1) (X2 : set T2) (Y1 : set T1) (Y2 : set T2) : (X1 `&` Y1) `*` (X2 `&` Y2) = X1 `*` X2 `&` Y1 `*` Y2. Proof. by rewrite predeqE => -[x y]; split=> [[[? ?] [*]//]|[] [? ?] [*]]. Qed. -Lemma setSM T1 T2 (C D : set T1) (A B : set T2) : +Lemma setSX T1 T2 (C D : set T1) (A B : set T2) : A `<=` B -> C `<=` D -> C `*` A `<=` D `*` B. Proof. by move=> AB CD x [] /CD Dx1 /AB Bx2. Qed. -Lemma setM_bigcupr T1 T2 I (F : I -> set T2) (P : set I) (A : set T1) : +Lemma setX_bigcupr T1 T2 I (F : I -> set T2) (P : set I) (A : set T1) : A `*` \bigcup_(i in P) F i = \bigcup_(i in P) (A `*` F i). Proof. rewrite predeqE => -[x y]; split; first by move=> [/= Ax [n Pn Fny]]; exists n. by move=> [n Pn [/= Ax Fny]]; split => //; exists n. Qed. -Lemma setM_bigcupl T1 T2 I (F : I -> set T2) (P : set I) (A : set T1) : +Lemma setX_bigcupl T1 T2 I (F : I -> set T2) (P : set I) (A : set T1) : \bigcup_(i in P) F i `*` A = \bigcup_(i in P) (F i `*` A). Proof. rewrite predeqE => -[x y]; split; first by move=> [[n Pn Fnx] Ax]; exists n. by move=> [n Pn [/= Ax Fny]]; split => //; exists n. Qed. -Lemma bigcupM1l T1 T2 (A1 : set T1) (A2 : T1 -> set T2) : - \bigcup_(i in A1) ([set i] `*` (A2 i)) = A1 `*`` A2. +Lemma bigcupX1l T1 T2 (A1 : set T1) (A2 : T1 -> set T2) : + \bigcup_(i in A1) ([set i] `*` A2 i) = A1 `*`` A2. Proof. by apply/predeqP => -[i j]; split=> [[? ? [/= -> //]]|[]]; exists i. Qed. -Lemma bigcupM1r T1 T2 (A1 : T2 -> set T1) (A2 : set T2) : +Lemma bigcupX1r 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. @@ -1198,6 +1204,30 @@ Notation setIv := setICr (only parsing). #[deprecated(since="mathcomp-analysis 1.2.0", note="Use notin_setE instead.")] Notation notin_set := notin_setE (only parsing). Arguments setU_id2r {T} C {A B}. +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to in_setX.")] +Notation in_setM := in_setX (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to setX0.")] +Notation setM0 := setX0 (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to set0X.")] +Notation set0M := set0X (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to setXTT.")] +Notation setMTT := setXTT (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to setXT.")] +Notation setMT := setXT (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to setTX.")] +Notation setTM := setTX (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to setXI.")] +Notation setMI := setXI (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to setX_bigcupr.")] +Notation setM_bigcupr := setX_bigcupr (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to setX_bigcupl.")] +Notation setM_bigcupl := setX_bigcupl (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to setSX.")] +Notation setSM := setSX (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to bigcupX1l.")] +Notation bigcupM1l := bigcupX1l (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to bigcupX1r.")] +Notation bigcupM1r := bigcupX1r (only parsing). Section set_order. Import Order.TTheory. @@ -1605,7 +1635,7 @@ Arguments sub_image_setI {aT rT f A B} t _. Lemma image2_subset {aT bT rT : Type} (f : aT -> bT -> rT) (A B : set aT) (C D : set bT) : A `<=` B -> C `<=` D -> [set f x y | x in A & y in C] `<=` [set f x y | x in B & y in D]. -Proof. by move=> AB CD; rewrite !image2E; apply: image_subset; exact: setSM. Qed. +Proof. by move=> AB CD; rewrite !image2E; apply: image_subset; exact: setSX. Qed. Lemma image_comp T1 T2 T3 (f : T1 -> T2) (g : T2 -> T3) A : g @` (f @` A) = (g \o f) @` A. @@ -1975,7 +2005,7 @@ Lemma setD_bigcupl (F : I -> set T) (P : set I) (A : set T) : \bigcup_(i in P) F i `\` A = \bigcup_(i in P) (F i `\` A). Proof. by rewrite setDE setI_bigcupl; under eq_bigcupr do rewrite -setDE. Qed. -Lemma bigcup_setM_dep {J : Type} (F : I -> J -> set T) +Lemma bigcup_setX_dep {J : Type} (F : I -> J -> set T) (P : set I) (Q : I -> set J) : \bigcup_(k in P `*`` Q) F k.1 k.2 = \bigcup_(i in P) \bigcup_(j in Q i) F i j. Proof. @@ -1983,9 +2013,9 @@ apply/predeqP => x; split=> [|[i Pi [j Pj Fijx]]]; last by exists (i, j). by move=> [[/= i j] [Pi Qj] Fijx]; exists i => //; exists j. Qed. -Lemma bigcup_setM {J : Type} (F : I -> J -> set T) (P : set I) (Q : set J) : +Lemma bigcup_setX {J : Type} (F : I -> J -> set T) (P : set I) (Q : set J) : \bigcup_(k in P `*` Q) F k.1 k.2 = \bigcup_(i in P) \bigcup_(j in Q) F i j. -Proof. exact: bigcup_setM_dep. Qed. +Proof. exact: bigcup_setX_dep. Qed. Lemma bigcup_bigcup T' (F : I -> set T) (P : set I) (G : T -> set T') : \bigcup_(i in \bigcup_(n in P) F n) G i = @@ -2034,6 +2064,11 @@ End bigop_lemmas. Arguments bigcup_setD1 {T I} x. Arguments bigcap_setD1 {T I} x. +#[deprecated(since="mathcomp-analysis 1.3.0",note="renamed to bigcup_setX_dep")] +Notation bigcup_setM_dep := bigcup_setX_dep (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0",note="renamed to bigcup_setX")] +Notation bigcup_setM := bigcup_setX (only parsing). + Lemma setD_bigcup {T} (I : eqType) (F : I -> set T) (P : set I) (j : I) : P j -> F j `\` \bigcup_(i in [set k | P k /\ k != j]) (F j `\` F i) = \bigcap_(i in P) F i. @@ -3285,16 +3320,22 @@ Lemma fst_set_fst A : A `<=` A.`1 \o fst. Proof. by move=> [x y]; exists y. Qed. Lemma snd_set_snd A: A `<=` A.`2 \o snd. Proof. by move=> [x y]; exists x. Qed. -Lemma fst_setM (X : set T1) (Y : set T2) : (X `*` Y).`1 `<=` X. +Lemma fst_setX (X : set T1) (Y : set T2) : (X `*` Y).`1 `<=` X. Proof. by move=> x [y [//]]. Qed. -Lemma snd_setM (X : set T1) (Y : set T2) : (X `*` Y).`2 `<=` Y. +Lemma snd_setX (X : set T1) (Y : set T2) : (X `*` Y).`2 `<=` Y. Proof. by move=> x [y [//]]. Qed. -Lemma fst_setMR (X : set T1) (Y : T1 -> set T2) : (X `*`` Y).`1 `<=` X. +Lemma fst_setXR (X : set T1) (Y : T1 -> set T2) : (X `*`` Y).`1 `<=` X. Proof. by move=> x [y [//]]. Qed. End product. +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to fst_setX.")] +Notation fst_setM := fst_setX (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to snd_setX.")] +Notation snd_setM := snd_setX (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to fst_setXR instead.")] +Notation fst_setMR := fst_setXR (only parsing). Section section. Variables (T1 T2 : Type). @@ -3322,25 +3363,25 @@ Proof. by rewrite predeqE /xsection => y; split => //=; rewrite inE. Qed. Lemma ysection0 y : ysection set0 y = set0. Proof. by rewrite predeqE /ysection => x; split => //=; rewrite inE. Qed. -Lemma in_xsectionM X1 X2 x : x \in X1 -> xsection (X1 `*` X2) x = X2. +Lemma in_xsectionX X1 X2 x : x \in X1 -> xsection (X1 `*` X2) x = X2. Proof. -move=> xX1; apply/seteqP; split=> [y /xsection_snd_set|]; first exact: snd_setM. +move=> xX1; apply/seteqP; split=> [y /xsection_snd_set|]; first exact: snd_setX. by move=> y X2y; rewrite /xsection/= inE; split=> //=; rewrite inE in xX1. Qed. -Lemma in_ysectionM X1 X2 y : y \in X2 -> ysection (X1 `*` X2) y = X1. +Lemma in_ysectionX X1 X2 y : y \in X2 -> ysection (X1 `*` X2) y = X1. Proof. -move=> yX2; apply/seteqP; split=> [x /ysection_fst_set|]; first exact: fst_setM. +move=> yX2; apply/seteqP; split=> [x /ysection_fst_set|]; first exact: fst_setX. by move=> x X1x; rewrite /ysection/= inE; split=> //=; rewrite inE in yX2. Qed. -Lemma notin_xsectionM X1 X2 x : x \notin X1 -> xsection (X1 `*` X2) x = set0. +Lemma notin_xsectionX X1 X2 x : x \notin X1 -> xsection (X1 `*` X2) x = set0. Proof. move=> xX1; rewrite /xsection /= predeqE => y; split => //. by rewrite /xsection/= inE => -[] /=; rewrite notin_setE in xX1. Qed. -Lemma notin_ysectionM X1 X2 y : y \notin X2 -> ysection (X1 `*` X2) y = set0. +Lemma notin_ysectionX X1 X2 y : y \notin X2 -> ysection (X1 `*` X2) y = set0. Proof. move=> yX2; rewrite /xsection /= predeqE => x; split => //. by rewrite /ysection/= inE => -[_]; rewrite notin_setE in yX2. @@ -3403,6 +3444,14 @@ Lemma ysection_preimage_fst (A : set T1) y : ysection (fst @^-1` A) y = A. Proof. by apply/seteqP; split; move=> x/=; rewrite /ysection/= inE. Qed. End section. +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to in_xsectionX.")] +Notation in_xsectionM := in_xsectionX (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to in_ysectionX.")] +Notation in_ysectionM := in_ysectionX (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to notin_xsectionX.")] +Notation notin_xsectionM := notin_xsectionX (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to notin_ysectionX.")] +Notation notin_ysectionM := notin_ysectionX (only parsing). Notation "B \; A" := ([set xy | exists2 z, A (xy.1, z) & B (z, xy.2)]) : classical_set_scope. diff --git a/classical/fsbigop.v b/classical/fsbigop.v index d0552d8a5..9df92abd8 100644 --- a/classical/fsbigop.v +++ b/classical/fsbigop.v @@ -504,9 +504,9 @@ Lemma pair_fsbig (R : Type) (idx : R) (op : Monoid.com_law idx) \big[op/idx]_(i \in P) \big[op/idx]_(j \in Q) F i j = \big[op/idx]_(p \in P `*` Q) F p.1 p.2. Proof. -move=> Pfin Qfin; have PQfin : finite_set (P `*` Q) by apply: finite_setM. +move=> Pfin Qfin; have PQfin : finite_set (P `*` Q) by exact: finite_setX. rewrite !fsbig_finite//=; under eq_bigr do rewrite fsbig_finite//=. -rewrite pair_big_dep_cond/= fset_setM//. +rewrite pair_big_dep_cond/= fset_setX//. apply: eq_fbigl => -[i j] //=; apply/imfset2P/idP; rewrite inE //=. by move=> [x + [y + [-> ->]]]; rewrite 4!inE/= !andbT/= => -> ->. move=> /andP[Pi Qi]; exists i; rewrite 2?inE ?andbT//. diff --git a/theories/esum.v b/theories/esum.v index 9df507fb1..3e7bde7fe 100644 --- a/theories/esum.v +++ b/theories/esum.v @@ -234,8 +234,8 @@ move=> a_ge0; apply/eqP; rewrite eq_le; apply/andP; split. apply: ub_ereal_sup => /= _ [Y [finY _] <-]; apply: ereal_sup_ubound => /=. set XYJ := [set z | z \in X `*` Y /\ z.2 \in J z.1]. have ? : finite_set XYJ. - apply: sub_finite_set (finite_setM finX finY) => z/=. - by rewrite /XYJ/= in_setM => -[/andP[] /[!inE]]. + apply: sub_finite_set (finite_setX finX finY) => z/=. + by rewrite /XYJ/= in_setX => -[/andP[] /[!inE]]. exists XYJ => /=; first by split => //= z; rewrite /XYJ/= 2!inE=> -[[/XI]]. rewrite [in RHS]fsbig_finite//= (exchange_big_dep xpredT)// pair_big_dep_cond. rewrite fsbig_finite//; apply: eq_fbigl => -[/= x y]; rewrite in_fset_set//. diff --git a/theories/function_spaces.v b/theories/function_spaces.v index a53f552e9..b9da21cc2 100644 --- a/theories/function_spaces.v +++ b/theories/function_spaces.v @@ -1418,7 +1418,7 @@ pose L := [set h | h @` ((K `&` closure P') `*` M) `<=` O]. exists (setT, P' `*` L). split => //; [exact: filterT|]; exists (P', L) => //; split => //. apply: open_nbhs_nbhs; split; first apply: compact_open_open => //. - apply: compact_setM => //; apply: compact_closedI => //. + apply: compact_setX => //; apply: compact_closedI => //. exact: closed_closure. by move=> ? [[a b] [[Ka /cPO +] Mb <-]] => /(_ _ Mb)/nbhs_singleton. move=> [b [a h]] [/= _ [Pa] +] Ma Ka; apply. diff --git a/theories/kernel.v b/theories/kernel.v index 1dcd54c6e..6dad64786 100644 --- a/theories/kernel.v +++ b/theories/kernel.v @@ -337,7 +337,7 @@ transitivity (\esum_(l in [set: nat] `*` [set: nat]) p l.1 l.2 x U). by rewrite kE// nneseries_esum. rewrite (reindex_esum [set: nat] _ f)//; last first. have := @bijTT _ _ f. - by rewrite -setTT_bijective/= -[in X in set_bij _ X _ -> _](@setMTT nat nat). + by rewrite -setTT_bijective/= -[in X in set_bij _ X _ -> _](@setXTT nat nat). by rewrite nneseries_esum// fun_true; exact: eq_esum. Qed. @@ -437,8 +437,8 @@ Let XY := [set A | measurable A /\ measurable_fun [set: X] (phi A)]. Let phiM (A : set X) B : phi (A `*` B) = (fun x => kD x B * (\1_A x)%:E). Proof. rewrite funeqE => x; rewrite indicE /phi/=. -have [xA|xA] := boolP (x \in A); first by rewrite mule1 in_xsectionM. -by rewrite mule0 notin_xsectionM// set0I measure0. +have [xA|xA] := boolP (x \in A); first by rewrite mule1 in_xsectionX. +by rewrite mule0 notin_xsectionX// set0I measure0. Qed. Lemma measurable_prod_subset_xsection_kernel : @@ -450,10 +450,10 @@ set C := [set A `*` B | A in measurable & B in measurable]. have CI : setI_closed C. move=> _ _ [X1 mX1 [X2 mX2 <-]] [Y1 mY1 [Y2 mY2 <-]]. exists (X1 `&` Y1); first exact: measurableI. - by exists (X2 `&` Y2); [exact: measurableI|rewrite setMI]. -have CT : C setT by exists setT => //; exists setT => //; rewrite setMTT. + by exists (X2 `&` Y2); [exact: measurableI|rewrite setXI]. +have CT : C setT by exists setT => //; exists setT => //; rewrite setXTT. have CXY : C `<=` XY. - move=> _ [A mA [B mB <-]]; split; first exact: measurableM. + move=> _ [A mA [B mB <-]]; split; first exact: measurableX. rewrite phiM. apply: emeasurable_funM => //; first exact/measurable_kernel/measurableI. by apply/EFin_measurable_fun; rewrite (_ : \1_ _ = mindic R mA). diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 0a8b66a1d..8f8bb8076 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -4624,14 +4624,14 @@ set C := [set A1 `*` A2 | A1 in measurable & A2 in measurable]. have CI : setI_closed C. move=> X Y [X1 mX1 [X2 mX2 <-{X}]] [Y1 mY1 [Y2 mY2 <-{Y}]]. exists (X1 `&` Y1); first exact: measurableI. - by exists (X2 `&` Y2); [exact: measurableI|rewrite setMI]. -have CT : C setT by exists setT => //; exists setT => //; rewrite setMTT. + by exists (X2 `&` Y2); [exact: measurableI|rewrite setXI]. +have CT : C setT by exists setT => //; exists setT => //; rewrite setXTT. have CB : C `<=` B. - move=> X [X1 mX1 [X2 mX2 <-{X}]]; split; first exact: measurableM. + move=> X [X1 mX1 [X2 mX2 <-{X}]]; split; first exact: measurableX. have -> : phi (X1 `*` X2) = (fun x => m2D X2 * (\1_X1 x)%:E)%E. rewrite funeqE => x; rewrite indicE /phi /m2/= /mrestr. - have [xX1|xX1] := boolP (x \in X1); first by rewrite mule1 in_xsectionM. - by rewrite mule0 notin_xsectionM// set0I measure0. + have [xX1|xX1] := boolP (x \in X1); first by rewrite mule1 in_xsectionX. + by rewrite mule0 notin_xsectionX// set0I measure0. exact/measurable_funeM/EFin_measurable_fun. suff lsystemB : lambda_system setT B by exact: lambda_system_subset. split => //; [exact: CB| |exact: xsection_ndseq_closed]. @@ -4665,14 +4665,14 @@ set C := [set A1 `*` A2 | A1 in measurable & A2 in measurable]. have CI : setI_closed C. move=> X Y [X1 mX1 [X2 mX2 <-{X}]] [Y1 mY1 [Y2 mY2 <-{Y}]]. exists (X1 `&` Y1); first exact: measurableI. - by exists (X2 `&` Y2); [exact: measurableI|rewrite setMI]. -have CT : C setT by exists setT => //; exists setT => //; rewrite setMTT. + by exists (X2 `&` Y2); [exact: measurableI|rewrite setXI]. +have CT : C setT by exists setT => //; exists setT => //; rewrite setXTT. have CB : C `<=` B. - move=> X [X1 mX1 [X2 mX2 <-{X}]]; split; first exact: measurableM. + move=> X [X1 mX1 [X2 mX2 <-{X}]]; split; first exact: measurableX. have -> : psi (X1 `*` X2) = (fun x => m1D X1 * (\1_X2 x)%:E)%E. rewrite funeqE => y; rewrite indicE /psi /m1/= /mrestr. - have [yX2|yX2] := boolP (y \in X2); first by rewrite mule1 in_ysectionM. - by rewrite mule0 notin_ysectionM// set0I measure0. + have [yX2|yX2] := boolP (y \in X2); first by rewrite mule1 in_ysectionX. + by rewrite mule0 notin_ysectionX// set0I measure0. exact/measurable_funeM/EFin_measurable_fun. suff lsystemB : lambda_system setT B by exact: lambda_system_subset. split => //; [exact: CB| |exact: ysection_ndseq_closed]. @@ -4704,9 +4704,9 @@ Proof. move: A; suff : measurable `<=` B by move=> + A => /[apply] -[]. have /sigma_finiteP [F [F_T F_nd F_oo]] := sigma_finiteT m2 => X mX. have -> : X = \bigcup_n (X `&` (setT `*` F n)). - by rewrite -setI_bigcupr -setM_bigcupr -F_T setMTT setIT. + by rewrite -setI_bigcupr -setX_bigcupr -F_T setXTT setIT. apply: xsection_ndseq_closed. - move=> m n mn; apply/subsetPset; apply: setIS; apply: setSM => //. + move=> m n mn; apply/subsetPset; apply: setIS; apply: setSX => //. exact/subsetPset/F_nd. move=> n; rewrite -/B; have [? ?] := F_oo n. pose m2Fn := mrestr m2 (F_oo n).1. @@ -4718,10 +4718,10 @@ have m2Fn_bounded : exists M, forall X, measurable X -> (m2Fn X < M%:E)%E. pose phi' A := m2Fn \o xsection A. pose B' := [set A | measurable A /\ measurable_fun setT (phi' A)]. have subset_B' : measurable `<=` B' by exact: measurable_prod_subset_xsection. -split=> [|_ Y mY]; first by apply: measurableI => //; exact: measurableM. +split=> [|_ Y mY]; first by apply: measurableI => //; exact: measurableX. have [_ /(_ measurableT Y mY)] := subset_B' X mX. have ->// : phi' X = m2 \o xsection (X `&` setT `*` F n). -by apply/funext => x/=; rewrite /phi' setTM xsectionI xsection_preimage_snd. +by apply/funext => x/=; rewrite /phi' setTX xsectionI xsection_preimage_snd. Qed. End measurable_fun_xsection. @@ -4739,9 +4739,9 @@ Proof. move: A; suff : measurable `<=` B by move=> + A => /[apply] -[]. have /sigma_finiteP[F [F_T F_nd F_oo]] := sigma_finiteT m1 => X mX. have -> : X = \bigcup_n (X `&` (F n `*` setT)). - by rewrite -setI_bigcupr -setM_bigcupl -F_T setMTT setIT. + by rewrite -setI_bigcupr -setX_bigcupl -F_T setXTT setIT. apply: ysection_ndseq_closed. - move=> m n mn; apply/subsetPset; apply: setIS; apply: setSM => //. + move=> m n mn; apply/subsetPset; apply: setIS; apply: setSX => //. exact/subsetPset/F_nd. move=> n; have [? ?] := F_oo n; rewrite -/B. pose m1Fn := mrestr m1 (F_oo n).1. @@ -4753,10 +4753,10 @@ have m1Fn_bounded : exists M, forall X, measurable X -> (m1Fn X < M%:E)%E. pose psi' A := m1Fn \o ysection A. pose B' := [set A | measurable A /\ measurable_fun setT (psi' A)]. have subset_B' : measurable `<=` B' by exact: measurable_prod_subset_ysection. -split=> [|_ Y mY]; first by apply: measurableI => //; exact: measurableM. +split=> [|_ Y mY]; first by apply: measurableI => //; exact: measurableX. have [_ /(_ measurableT Y mY)] := subset_B' X mX. have ->// : psi' X = m1 \o (ysection (X `&` F n `*` setT)). -by apply/funext => y/=; rewrite /psi' setMT ysectionI// ysection_preimage_fst. +by apply/funext => y/=; rewrite /psi' setXT ysectionI// ysection_preimage_fst. Qed. End measurable_fun_ysection. @@ -4818,7 +4818,7 @@ Proof. move=> mA1 mA2 /=; rewrite /product_measure1 /=. rewrite (eq_integral (fun x => (\1_A1 x)%:E * m2 A2)); last first. by move=> x _; rewrite indicE; have [xA1|xA1] /= := boolP (x \in A1); - [rewrite in_xsectionM// mul1e|rewrite mul0e notin_xsectionM]. + [rewrite in_xsectionX// mul1e|rewrite mul0e notin_xsectionX]. rewrite ge0_integralZr//; last by move=> x _; rewrite lee_fin. - by rewrite integral_indic// setIT. - exact: measurableT_comp. @@ -4837,13 +4837,13 @@ Proof. have /sigma_finiteP[F [TF ndF Foo]] := sigma_finiteT m1. have /sigma_finiteP[G [TG ndG Goo]] := sigma_finiteT m2. exists (fun n => F n `*` G n). - rewrite -setMTT TF TG predeqE => -[x y]; split. + rewrite -setXTT TF TG predeqE => -[x y]; split. move=> [/= [n _ Fnx] [k _ Gky]]; exists (maxn n k) => //; split. - by move: x Fnx; exact/subsetPset/ndF/leq_maxl. - by move: y Gky; exact/subsetPset/ndG/leq_maxr. by move=> [n _ []/= ? ?]; split; exists n. move=> k; have [? ?] := Foo k; have [? ?] := Goo k. -split; first exact: measurableM. +split; first exact: measurableX. by rewrite product_measure1E// lte_mul_pinfty// ge0_fin_numE. Qed. @@ -4860,7 +4860,7 @@ move=> m'E. have /sigma_finiteP[F [TF ndF Foo]] := sigma_finiteT m1. have /sigma_finiteP[G [TG ndG Goo]] := sigma_finiteT m2. have UFGT : \bigcup_k (F k `*` G k) = setT. - rewrite -setMTT TF TG predeqE => -[x y]; split. + rewrite -setXTT TF TG predeqE => -[x y]; split. by move=> [n _ []/= ? ?]; split; exists n. move=> [/= [n _ Fnx] [k _ Gky]]; exists (maxn n k) => //; split. - by move: x Fnx; exact/subsetPset/ndF/leq_maxl. @@ -4869,7 +4869,7 @@ pose C : set (set (T1 * T2)) := [set C | exists A, measurable A /\ exists B, measurable B /\ C = A `*` B]. have CI : setI_closed C. move=> /= _ _ [X1 [mX1 [X2 [mX2 ->]]]] [Y1 [mY1 [Y2 [mY2 ->]]]]. - rewrite -setMI; exists (X1 `&` Y1); split; first exact: measurableI. + rewrite -setXI; exists (X1 `&` Y1); split; first exact: measurableI. by exists (X2 `&` Y2); split => //; exact: measurableI. move=> X mX; apply: (measure_unique C (fun n => F n `*` G n)) => //. - rewrite measurable_prod_measurableType //; congr (<>). @@ -4930,7 +4930,7 @@ Lemma product_measure2E (A1 : set T1) (A2 : set T2) (mA1 : measurable A1) (mA2 : measurable A2) : (m1 \x^ m2) (A1 `*` A2) = m1 A1 * m2 A2. Proof. -have mA1A2 : measurable (A1 `*` A2) by apply: measurableM. +have mA1A2 : measurable (A1 `*` A2) by apply: measurableX. transitivity (\int[m2]_y (m1 \o ysection (A1 `*` A2)) y) => //. rewrite (_ : _ \o _ = fun y => m1 A1 * (\1_A2 y)%:E). rewrite ge0_integralZl//. @@ -4938,8 +4938,8 @@ rewrite (_ : _ \o _ = fun y => m1 A1 * (\1_A2 y)%:E). - exact: measurableT_comp. - by move=> y _; rewrite lee_fin. rewrite funeqE => y; rewrite indicE. -have [yA2|yA2] := boolP (y \in A2); first by rewrite mule1 /= in_ysectionM. -by rewrite mule0 /= notin_ysectionM. +have [yA2|yA2] := boolP (y \in A2); first by rewrite mule1 /= in_ysectionX. +by rewrite mule0 /= notin_ysectionX. Qed. End product_measure2E. diff --git a/theories/measure.v b/theories/measure.v index cb4789ba5..622768f86 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -2639,8 +2639,8 @@ have mdW A : measurable A -> measurable_fin_trivIset A. have mdI : setI_closed measurable_fin_trivIset. move=> _ _ [A [-> Am Afin Atriv]] [B [-> Bm Bfin Btriv]]. rewrite setI_bigcupl; under eq_bigcupr do rewrite setI_bigcupr. - rewrite -bigcup_setM -(bigcup_image _ _ id). - eexists; split; [reflexivity | | exact/finite_image/finite_setM |]. + rewrite -bigcup_setX -(bigcup_image _ _ id). + eexists; split; [reflexivity | | exact/finite_image/finite_setX |]. by move=> _ [X [? ?] <-]; apply: measurableI; [apply: Am|apply: Bm]. apply: trivIset_sets => -[a b] [a' b']/= [Xa Xb] [Xa' Xb']; rewrite setIACA. by move=> [x [Ax Bx]]; rewrite (Atriv a a') 1?(Btriv b b')//; exists x. @@ -2658,9 +2658,9 @@ have mdU : fin_trivIset_closed measurable_fin_trivIset. have /(_ _ (set_mem _))/cid-/(all_sig_cond_dep (fun=> set0)) [G /(_ _ (mem_set _))GP] := Fm _ _. under eq_bigcupr => i Di do case: (GP i Di) => ->. - rewrite -bigcup_setM_dep -(bigcup_image _ _ id); eexists; split=> //. + rewrite -bigcup_setX_dep -(bigcup_image _ _ id); eexists; split=> //. - by move=> _ [i [Di Gi] <-]; have [_ + _ _] := GP i.1 Di; apply. - - by apply: finite_image; apply: finite_setMR=> // i Di; have [] := GP i Di. + - by apply: finite_image; apply: finite_setXR=> // i Di; have [] := GP i Di. apply: trivIset_sets => -[i X] [j Y] /= [Di Gi] [Dj Gj] XYN0. suff eqij : i = j. by rewrite {i}eqij in Di Gi *; have [_ _ _ /(_ _ _ _ _ XYN0)->] := GP j Dj. @@ -2980,7 +2980,7 @@ rewrite /Rmu -(eq_eseriesr (fun _ _ => esum_fset _ _))//; last first. rewrite nneseries_esum ?esum_esum//=; last by move=> *; rewrite esum_ge0. set K := _ `*`` _. have /ppcard_eqP[f] : (K #= [set: nat])%card. - apply: cardMR_eq_nat => [|i]. + apply: cardXR_eq_nat => [|i]. by rewrite (_ : [set _ | true] = setT)//; exact/predeqP. split; first by apply/finite_set_countable; exact: decomp_finite_set. exact/set0P/decompN0. @@ -3083,9 +3083,9 @@ have DUBm i : measurable (seqDU B i : set (SetRing.type T)). do 1?apply: bigsetU_measurable => *; apply: sub_gen_smallest. rewrite XE; move: (XE); rewrite seqDU_bigcup_eq. under eq_bigcupr do rewrite -[seqDU B _]cover_decomp//. -rewrite -bigcup_setM_dep; set K := _ `*`` _. +rewrite -bigcup_setX_dep; set K := _ `*`` _. have /ppcard_eqP[f] : (K #= [set: nat])%card. - apply: cardMR_eq_nat=> // i; split; last by apply/set0P; rewrite decompN0. + apply: cardXR_eq_nat=> // i; split; last by apply/set0P; rewrite decompN0. exact/finite_set_countable/decomp_finite_set. pose f' := f^-1%FUN; rewrite -(image_eq [bij of f'])/= bigcup_image/=. pose g n := (f' n).2; have fVtriv : trivIset [set: nat] g. @@ -4801,7 +4801,7 @@ rewrite ?lb_ereal_inf// => _ [F [Fm XS] <-]; rewrite ereal_inf_lbound//; last fi by rewrite (eq_eseriesr (fun _ _ => RmuE _ (Fm _))). pose K := [set: nat] `*`` fun i => decomp (F i). have /ppcard_eqP[f] : (K #= [set: nat])%card. - apply: cardMR_eq_nat => // i; split; last by apply/set0P; rewrite decompN0. + apply: cardXR_eq_nat => // i; split; last by apply/set0P; rewrite decompN0. by apply: finite_set_countable => //; exact: decomp_finite_set. pose g i := (f^-1%FUN i).2; exists g; first split. - move=> k; have [/= _ /mem_set] : K (f^-1%FUN k) by apply: funS. @@ -5034,17 +5034,19 @@ Notation "p .-prod.-measurable" := ((p.-prod).-measurable : set (set (_ * _))) : classical_set_scope. -Lemma measurableM d1 d2 (T1 : semiRingOfSetsType d1) (T2 : semiRingOfSetsType d2) +Lemma measurableX d1 d2 (T1 : semiRingOfSetsType d1) (T2 : semiRingOfSetsType d2) (A : set T1) (B : set T2) : measurable A -> measurable B -> measurable (A `*` B). Proof. move=> mA mB. have -> : A `*` B = (A `*` setT) `&` (setT `*` B) :> set (T1 * T2). - by rewrite -{1}(setIT A) -{1}(setTI B) setMI. -rewrite setMT setTM; apply: measurableI. + by rewrite -{1}(setIT A) -{1}(setTI B) setXI. +rewrite setXT setTX; apply: measurableI. - by apply: sub_sigma_algebra; left; exists A => //; rewrite setTI. - by apply: sub_sigma_algebra; right; exists B => //; rewrite setTI. Qed. +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `measurableX`")] +Notation measurableM := measurableX (only parsing). Section product_salgebra_algebraOfSetsType. Context d1 d2 (T1 : algebraOfSetsType d1) (T2 : algebraOfSetsType d2). @@ -5065,7 +5067,7 @@ rewrite eqEsubset; split. by move=> _ [Y MY <-]; exists setT; rewrite /M1 //; exists Y. by apply; exact: sub_sigma_algebra. apply: smallest_sub; first exact: smallest_sigma_algebra. -by move=> _ [A MA] [B MB] <-; apply: measurableM => //; exact: sub_sigma_algebra. +by move=> _ [A MA] [B MB] <-; apply: measurableX => //; exact: sub_sigma_algebra. Qed. End product_salgebra_algebraOfSetsType. diff --git a/theories/normedtype.v b/theories/normedtype.v index 79849cd5d..9c5618ddb 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -1896,7 +1896,7 @@ Notation lipschitz f := [lipschitz f x | x in setT]. Lemma lipschitz_set0 (K : numFieldType) (V W : normedModType K) (f : V -> W) : [lipschitz f x | x in set0]. -Proof. by apply: nearW; rewrite setM0 => ?; apply: globally0. Qed. +Proof. by apply: nearW; rewrite setX0 => ?; apply: globally0. Qed. Lemma lipschitz_set1 (K : numFieldType) (V W : normedModType K) (f : V -> W) (a : V) : [lipschitz f x | x in [set a]]. diff --git a/theories/topology.v b/theories/topology.v index fafdc65ba..b6bf97740 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -3015,7 +3015,7 @@ Unshelve. all: by end_near. Qed. End near_covering. -Lemma compact_setM {U V : topologicalType} (P : set U) (Q : set V) : +Lemma compact_setX {U V : topologicalType} (P : set U) (Q : set V) : compact P -> compact Q -> compact (P `*` Q). Proof. rewrite !compact_near_coveringP => cptP cptQ I F Pr Ff cvfPQ. @@ -3028,6 +3028,8 @@ exists (N2, N1`*`G); first by split => //; exists (N1, G). case=> a [b i] /= [N2a [N1b]] Gi. by apply: (ngPr (b, a, i)); split => //; exact: N1N2N. Unshelve. all: by end_near. Qed. +#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `compact_setX`")] +Notation compact_setM := compact_setX (only parsing). Section UltraFilters. @@ -4302,13 +4304,13 @@ Qed. Lemma prod_ent_filter : Filter prod_ent. Proof. have prodF := filter_prod_filter (@entourage_pfilter U) (@entourage_pfilter V). -split; rewrite /prod_ent; last 1 first. +split; rewrite /prod_ent. +- by rewrite -setXTT; apply: prod_entP filterT filterT. +- move=> A B /= entA entB; apply: filterS (filterI entA entB) => xy []. + move=> [zt Azt ztexy] [zt' Bzt' zt'exy]; exists zt => //; split=> //. + move/eqP: ztexy; rewrite -zt'exy !xpair_eqE. + by rewrite andbACA -!xpair_eqE -!surjective_pairing => /eqP->. - by move=> A B sAB /=; apply: filterS => ? [xy /sAB ??]; exists xy. -- by rewrite -setMTT; apply: prod_entP filterT filterT. -move=> A B /= entA entB; apply: filterS (filterI entA entB) => xy []. -move=> [zt Azt ztexy] [zt' Bzt' zt'exy]; exists zt => //; split=> //. -move/eqP: ztexy; rewrite -zt'exy !xpair_eqE. -by rewrite andbACA -!xpair_eqE -!surjective_pairing => /eqP->. Qed. Lemma prod_ent_refl A : prod_ent A -> [set xy | xy.1 = xy.2] `<=` A. From b6d9925aca147649eafda1aab4fcd81cf6b1a5d1 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sat, 3 Aug 2024 23:11:12 +0900 Subject: [PATCH 3/3] setY notation --- classical/classical_sets.v | 30 +++++++++++++----------------- theories/measure.v | 2 +- 2 files changed, 14 insertions(+), 18 deletions(-) diff --git a/classical/classical_sets.v b/classical/classical_sets.v index bd448d3fd..25b8c810b 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -42,7 +42,7 @@ From mathcomp Require Import mathcomp_extra boolp. (* | `` `\|` `` |==| $\cup$ *) (* | `` `&` `` |==| $\cap$ *) (* | `` `\` `` |==| set difference *) -(* | `` `^` `` |==| symmetric difference *) +(* | `` `+` `` |==| symmetric difference *) (* | `` ~` `` |==| set complement *) (* | `` `<=` `` |==| $\subseteq$ *) (* | `` f @` A `` |==| image by f of A *) @@ -245,11 +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). -*) +Reserved Notation "A `+` B" (at level 54, left associativity). Reserved Notation "\bigcup_ ( i < n ) F" (at level 41, F at level 41, i, n at level 50, format "'[' \bigcup_ ( i < n ) '/ ' F ']'"). @@ -410,7 +406,7 @@ Notation "[ 'disjoint' A & B ]" := (disj_set A B) : classical_set_scope. Definition setY {T : Type} (A B : set T) := (A `\` B) `|` (B `\` A). Arguments setY _ _ _ _ /. -Notation "A `^` B" := (setY A B) : classical_set_scope. +Notation "A `+` B" := (setY A B) : classical_set_scope. Notation "'`I_' n" := [set k | is_true (k < n)%N]. @@ -1135,16 +1131,16 @@ Proof. by move=> A; rewrite /setY setD0 set0D setU0. Qed. Lemma set0Y : left_id set0 (@setY T). Proof. by move=> A; rewrite /setY set0D setD0 set0U. Qed. -Lemma setYK A : A `^` A = set0. +Lemma setYK A : A `+` A = set0. Proof. by rewrite /setY setDv setU0. Qed. Lemma setYC : commutative (@setY T). Proof. by move=> A B; rewrite /setY setUC. Qed. -Lemma setYTC A : A `^` [set: T] = ~` A. +Lemma setYTC A : A `+` [set: T] = ~` A. Proof. by rewrite /setY setDT set0U setTD. Qed. -Lemma setTYC A : [set: T] `^` A = ~` A. +Lemma setTYC A : [set: T] `+` A = ~` A. Proof. by rewrite setYC setYTC. Qed. Lemma setYA : associative (@setY T). @@ -1164,34 +1160,34 @@ Qed. Lemma setIYr : right_distributive (@setI T) (@setY T). Proof. by move=> A B C; rewrite setIC setIYl -2!(setIC A). Qed. -Lemma setY_def A B : A `^` B = (A `\` B) `|` (B `\` A). +Lemma setY_def A B : A `+` B = (A `\` B) `|` (B `\` A). Proof. by []. Qed. -Lemma setYE A B : A `^` B = (A `|` B) `\` (A `&` B). +Lemma setYE A B : A `+` B = (A `|` B) `\` (A `&` B). Proof. rewrite /setY; apply/seteqP; split => x/=; by have [|] := pselect (A x); have [|] := pselect (B x); tauto. Qed. -Lemma setYU A B : (A `^` B) `^` (A `&` B) = A `|` B. +Lemma setYU A B : (A `+` B) `+` (A `&` B) = A `|` B. Proof. rewrite /setY; apply/seteqP; split => x/=; by have [|] := pselect (A x); have [|] := pselect (B x); tauto. Qed. -Lemma setYI A B : (A `|` B) `\` (A `^` B) = A `&` B. +Lemma setYI A B : (A `|` B) `\` (A `+` B) = A `&` B. Proof. rewrite /setY; apply/seteqP; split => x/=; by have [|] := pselect (A x); have [|] := pselect (B x); tauto. Qed. -Lemma setYD A B : A `^` (A `&` B) = A `\` B. +Lemma setYD A B : A `+` (A `&` B) = A `\` B. Proof. by rewrite /setY; apply/seteqP; split => x/=; tauto. Qed. -Lemma setYCT A : A `^` ~` A = [set: T]. +Lemma setYCT A : A `+` ~` A = [set: T]. Proof. by rewrite /setY setDE setCK setIid setDE setIid setUv. Qed. -Lemma setCYT A : ~` A `^` A = [set: T]. +Lemma setCYT A : ~` A `+` A = [set: T]. Proof. by rewrite setYC setYCT. Qed. End basic_lemmas. diff --git a/theories/measure.v b/theories/measure.v index 622768f86..9079ab93a 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -358,7 +358,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 setY_closed := forall A B, G A -> G B -> G (A `^` B). +Definition setY_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)) ->