Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

setX -> setY; setM -> setX #1276

Merged
merged 3 commits into from
Aug 6, 2024
Merged

setX -> setY; setM -> setX #1276

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
589d35a
setX -> setY
affeldt-aist Aug 1, 2024
87940c8
setM -> setX
affeldt-aist Aug 1, 2024
b6d9925
setY notation
affeldt-aist Aug 3, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
51 changes: 47 additions & 4 deletions CHANGELOG_UNRELEASED.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 ``` `^` ```
Copy link
Member

@CohenCyril CohenCyril Aug 1, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I am also going to argue that ^ generally means exponential and I would rather associate notation B `^` A to set_fun A B. For setY maybe we can pick y for now?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Or `+` ?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

FWIW, the notation for exclusive or in ssrbool is _ (+) _

+ 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`
Expand Down Expand Up @@ -211,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`:
Expand Down
73 changes: 46 additions & 27 deletions classical/cardinality.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -687,23 +687,26 @@ 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 *.
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.
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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).
Expand All @@ -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 => ? ->.
Expand Down
Loading
Loading