Skip to content

Commit

Permalink
setM -> setX
Browse files Browse the repository at this point in the history
  • Loading branch information
affeldt-aist committed Aug 1, 2024
1 parent 589d35a commit 87940c8
Show file tree
Hide file tree
Showing 11 changed files with 233 additions and 119 deletions.
42 changes: 42 additions & 0 deletions CHANGELOG_UNRELEASED.md
Original file line number Diff line number Diff line change
Expand Up @@ -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`:
Expand Down
73 changes: 46 additions & 27 deletions classical/cardinality.v
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

0 comments on commit 87940c8

Please sign in to comment.