feat(set_theory/cardinal/finite): prove lemmas to handle part_enat.ca…

…rd (#19198)

Prove some lemmas that allow to handle part_enat.card of finite cardinals,
analogous to those about nat.card



Co-authored-by: Antoine Chambert-Loir <antoine.chambert-loir@math.univ-paris-diderot.fr>

src/data/finite/card.lean

@@ -158,6 +158,18 @@ by { haveI := fintype.of_finite α, simpa using fintype.card_subtype_lt hx }
 
 end finite
 
+namespace part_enat
+
+lemma card_eq_coe_nat_card (α : Type*) [finite α] : card α = nat.card α :=
+begin
+  unfold part_enat.card,
+  apply symm,
+  rw cardinal.coe_nat_eq_to_part_enat_iff,
+  exact finite.cast_card_eq_mk ,
+end
+
+end part_enat
+
 namespace set
 
 lemma card_union_le (s t : set α) : nat.card ↥(s ∪ t) ≤ nat.card s + nat.card t :=

src/data/nat/part_enat.lean

@@ -380,6 +380,9 @@ begin
   apply_mod_cast nat.lt_of_succ_le, apply_mod_cast h
 end
 
+lemma coe_succ_le_iff {n : ℕ} {e : part_enat} : ↑n.succ ≤ e ↔ ↑n < e:=
+by rw [nat.succ_eq_add_one n, nat.cast_add, nat.cast_one, add_one_le_iff_lt (coe_ne_top n)]
+
 lemma lt_add_one_iff_lt {x y : part_enat} (hx : x ≠ ⊤) : x < y + 1 ↔ x ≤ y :=
 begin
   split, exact le_of_lt_add_one,
@@ -388,6 +391,9 @@ begin
   apply_mod_cast nat.lt_succ_of_le, apply_mod_cast h
 end
 
+lemma lt_coe_succ_iff_le {x : part_enat} {n : ℕ} (hx : x ≠ ⊤) : x < n.succ ↔ x ≤ n :=
+by rw [nat.succ_eq_add_one n, nat.cast_add, nat.cast_one, lt_add_one_iff_lt hx]
+
 lemma add_eq_top_iff {a b : part_enat} : a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤ :=
 by apply part_enat.cases_on a; apply part_enat.cases_on b;
   simp; simp only [(nat.cast_add _ _).symm, part_enat.coe_ne_top]; simp

src/set_theory/cardinal/basic.lean

@@ -1215,6 +1215,10 @@ by rw [to_nat_apply_of_lt_aleph_0 h, ← classical.some_spec (lt_aleph_0.1 h)]
 lemma cast_to_nat_of_aleph_0_le {c : cardinal} (h : ℵ₀ ≤ c) : ↑c.to_nat = (0 : cardinal) :=
 by rw [to_nat_apply_of_aleph_0_le h, nat.cast_zero]
 
+lemma to_nat_eq_iff_eq_of_lt_aleph_0 {c d : cardinal} (hc : c < ℵ₀) (hd : d < ℵ₀) :
+  c.to_nat = d.to_nat ↔ c = d :=
+by rw [←nat_cast_inj, cast_to_nat_of_lt_aleph_0 hc, cast_to_nat_of_lt_aleph_0 hd]
+
 lemma to_nat_le_iff_le_of_lt_aleph_0 {c d : cardinal} (hc : c < ℵ₀) (hd : d < ℵ₀) :
   c.to_nat ≤ d.to_nat ↔ c ≤ d :=
 by rw [←nat_cast_le, cast_to_nat_of_lt_aleph_0 hc, cast_to_nat_of_lt_aleph_0 hd]
@@ -1357,10 +1361,84 @@ to_part_enat_apply_of_aleph_0_le (infinite_iff.1 h)
 @[simp] theorem aleph_0_to_part_enat : to_part_enat ℵ₀ = ⊤ :=
 to_part_enat_apply_of_aleph_0_le le_rfl
 
+lemma to_part_enat_eq_top_iff_le_aleph_0 {c : cardinal} :
+  to_part_enat c = ⊤ ↔ aleph_0 ≤ c :=
+begin
+  cases lt_or_ge c aleph_0 with hc hc,
+  simp only [to_part_enat_apply_of_lt_aleph_0 hc, part_enat.coe_ne_top, false_iff, not_le, hc],
+  simp only [to_part_enat_apply_of_aleph_0_le hc, eq_self_iff_true, true_iff],
+  exact hc,
+end
+
+lemma to_part_enat_le_iff_le_of_le_aleph_0 {c c' : cardinal} (h : c ≤ aleph_0) :
+  to_part_enat c ≤ to_part_enat c' ↔ c ≤ c' :=
+begin
+  cases lt_or_ge c aleph_0 with hc hc,
+  rw to_part_enat_apply_of_lt_aleph_0 hc,
+  cases lt_or_ge c' aleph_0 with hc' hc',
+  { rw to_part_enat_apply_of_lt_aleph_0 hc',
+    rw part_enat.coe_le_coe,
+    exact to_nat_le_iff_le_of_lt_aleph_0 hc hc', },
+  { simp only [to_part_enat_apply_of_aleph_0_le hc',
+    le_top, true_iff],
+    exact le_trans h hc', },
+  { rw to_part_enat_apply_of_aleph_0_le hc,
+    simp only [top_le_iff, to_part_enat_eq_top_iff_le_aleph_0,
+    le_antisymm h hc], },
+end
+
+lemma to_part_enat_le_iff_le_of_lt_aleph_0 {c c' : cardinal} (hc' : c' < aleph_0) :
+  to_part_enat c ≤ to_part_enat c' ↔ c ≤ c' :=
+begin
+  cases lt_or_ge c aleph_0 with hc hc,
+  { rw to_part_enat_apply_of_lt_aleph_0 hc,
+    rw to_part_enat_apply_of_lt_aleph_0 hc',
+    rw part_enat.coe_le_coe,
+    exact to_nat_le_iff_le_of_lt_aleph_0 hc hc', },
+  { rw to_part_enat_apply_of_aleph_0_le hc,
+    simp only [top_le_iff, to_part_enat_eq_top_iff_le_aleph_0],
+    rw [← not_iff_not, not_le, not_le],
+    simp only [hc', lt_of_lt_of_le hc' hc], },
+end
+
+lemma to_part_enat_eq_iff_eq_of_le_aleph_0 {c c' : cardinal}
+  (hc : c ≤ aleph_0) (hc' : c' ≤ aleph_0) :
+  to_part_enat c = to_part_enat c' ↔ c = c' := by
+rw [le_antisymm_iff, le_antisymm_iff,
+  to_part_enat_le_iff_le_of_le_aleph_0 hc, to_part_enat_le_iff_le_of_le_aleph_0 hc']
+
+lemma to_part_enat_mono {c c' : cardinal} (h : c ≤ c') :
+  to_part_enat c ≤ to_part_enat c' :=
+begin
+  cases lt_or_ge c aleph_0 with hc hc,
+  rw to_part_enat_apply_of_lt_aleph_0 hc,
+  cases lt_or_ge c' aleph_0 with hc' hc',
+  rw to_part_enat_apply_of_lt_aleph_0 hc',
+  simp only [part_enat.coe_le_coe],
+  exact to_nat_le_of_le_of_lt_aleph_0 hc' h,
+  rw to_part_enat_apply_of_aleph_0_le hc',
+  exact le_top,
+  rw [to_part_enat_apply_of_aleph_0_le hc,
+  to_part_enat_apply_of_aleph_0_le (le_trans hc h)],
+end
+
 lemma to_part_enat_surjective : surjective to_part_enat :=
 λ x, part_enat.cases_on x ⟨ℵ₀, to_part_enat_apply_of_aleph_0_le le_rfl⟩ $
   λ n, ⟨n, to_part_enat_cast n⟩
 
+lemma to_part_enat_lift (c : cardinal.{v}) : (lift.{u v} c).to_part_enat = c.to_part_enat :=
+begin
+  cases lt_or_ge c ℵ₀ with hc hc,
+  { rw [to_part_enat_apply_of_lt_aleph_0 hc, cardinal.to_part_enat_apply_of_lt_aleph_0 _],
+    simp only [to_nat_lift],
+    rw [← lift_aleph_0, lift_lt], exact hc },
+  { rw [to_part_enat_apply_of_aleph_0_le hc, cardinal.to_part_enat_apply_of_aleph_0_le _],
+  rw [← lift_aleph_0, lift_le], exact hc }
+end
+
+lemma to_part_enat_congr {β : Type v} (e : α ≃ β) : (#α).to_part_enat = (#β).to_part_enat :=
+by rw [←to_part_enat_lift, lift_mk_eq.mpr ⟨e⟩, to_part_enat_lift]
+
 lemma mk_to_part_enat_eq_coe_card [fintype α] : (#α).to_part_enat = fintype.card α :=
 by simp
 
@@ -1369,7 +1447,8 @@ lemma mk_int : #ℤ = ℵ₀ := mk_denumerable ℤ
 lemma mk_pnat : #ℕ+ = ℵ₀ := mk_denumerable ℕ+
 
 /-- **König's theorem** -/
-theorem sum_lt_prod {ι} (f g : ι → cardinal) (H : ∀ i, f i < g i) : sum f < prod g :=
+theorem sum_lt_prod {ι} (f g : ι → cardinal) (H : ∀ i, f i < g i) :
+sum f < prod g :=
 lt_of_not_ge $ λ ⟨F⟩, begin
   haveI : inhabited (Π (i : ι), (g i).out),
   { refine ⟨λ i, classical.choice $ mk_ne_zero_iff.1 _⟩,

src/set_theory/cardinal/finite.lean

@@ -120,4 +120,92 @@ lemma card_eq_coe_fintype_card [fintype α] : card α = fintype.card α := mk_to
 @[simp]
 lemma card_eq_top_of_infinite [infinite α] : card α = ⊤ := mk_to_part_enat_of_infinite
 
+lemma card_congr {α : Type*} {β : Type*} (f : α ≃ β) :
+  part_enat.card α = part_enat.card β :=
+cardinal.to_part_enat_congr f
+
+lemma card_ulift (α : Type*) : card (ulift α) = card α :=
+card_congr equiv.ulift
+
+@[simp] lemma card_plift (α : Type*) : card (plift α) = card α :=
+card_congr equiv.plift
+
+lemma card_image_of_inj_on {α : Type*} {β : Type*} {f : α → β} {s : set α} (h : set.inj_on f s) :
+  card (f '' s) = card s :=
+card_congr (equiv.set.image_of_inj_on f s h).symm
+
+lemma card_image_of_injective {α : Type*} {β : Type*}
+  (f : α → β) (s : set α) (h : function.injective f) :
+  card (f '' s) = card s :=
+card_image_of_inj_on (set.inj_on_of_injective h s)
+
+-- Should I keep the 6 following lemmas ?
+@[simp]
+lemma _root_.cardinal.coe_nat_le_to_part_enat_iff {n : ℕ} {c : cardinal} :
+  ↑n ≤ to_part_enat c ↔ ↑n ≤ c :=
+by rw [← to_part_enat_cast n, to_part_enat_le_iff_le_of_le_aleph_0 (le_of_lt (nat_lt_aleph_0 n))]
+
+@[simp]
+lemma _root_.cardinal.to_part_enat_le_coe_nat_iff {c : cardinal} {n : ℕ} :
+  to_part_enat c ≤ n ↔ c ≤ n :=
+by rw [← to_part_enat_cast n,
+ to_part_enat_le_iff_le_of_lt_aleph_0 (nat_lt_aleph_0 n)]
+
+@[simp]
+lemma _root_.cardinal.coe_nat_eq_to_part_enat_iff {n : ℕ} {c : cardinal} :
+  ↑n = to_part_enat c ↔ ↑n = c :=
+by rw [le_antisymm_iff, le_antisymm_iff,
+  cardinal.coe_nat_le_to_part_enat_iff,  cardinal.to_part_enat_le_coe_nat_iff]
+
+@[simp]
+lemma _root_.cardinal.to_part_enat_eq_coe_nat_iff {c : cardinal} {n : ℕ} :
+  to_part_enat c = n ↔ c = n:=
+by rw [eq_comm, cardinal.coe_nat_eq_to_part_enat_iff, eq_comm]
+
+@[simp]
+lemma _root_.cardinal.coe_nat_lt_coe_iff_lt {n : ℕ} {c : cardinal} :
+  ↑n < to_part_enat c ↔ ↑n < c :=
+by simp only [← not_le, cardinal.to_part_enat_le_coe_nat_iff]
+
+@[simp]
+lemma _root_.cardinal.lt_coe_nat_iff_lt {n : ℕ} {c : cardinal} :
+  to_part_enat c < n ↔ c < n :=
+by simp only [← not_le, cardinal.coe_nat_le_to_part_enat_iff]
+
+lemma card_eq_zero_iff_empty (α : Type*) : card α = 0 ↔ is_empty α :=
+begin
+  rw ← cardinal.mk_eq_zero_iff,
+  conv_rhs { rw ← nat.cast_zero },
+  rw ← cardinal.to_part_enat_eq_coe_nat_iff,
+  simp only [part_enat.card, nat.cast_zero]
+end
+
+lemma card_le_one_iff_subsingleton (α : Type*) : card α ≤ 1 ↔ subsingleton α :=
+begin
+  rw ← le_one_iff_subsingleton,
+  conv_rhs { rw ← nat.cast_one},
+  rw ← cardinal.to_part_enat_le_coe_nat_iff,
+  simp only [part_enat.card, nat.cast_one]
+end
+
+lemma one_lt_card_iff_nontrivial (α : Type*) : 1 < card α ↔ nontrivial α :=
+begin
+  rw ← one_lt_iff_nontrivial,
+  conv_rhs { rw ← nat.cast_one},
+  rw ← cardinal.coe_nat_lt_coe_iff_lt,
+  simp only [part_enat.card, nat.cast_one]
+end
+
+lemma is_finite_of_card {α : Type*} {n : ℕ} (hα : part_enat.card α = n) :
+  finite α :=
+begin
+  apply or.resolve_right (finite_or_infinite α),
+  intro h, resetI,
+  apply part_enat.coe_ne_top n,
+  rw ← hα,
+  exact part_enat.card_eq_top_of_infinite,
+end
+
+
+
 end part_enat