Потужність множин

Аналіз I, Розділ 3.6: Кардинальність множин

Я (прим. перекл. Терренс Тао) намагався зробити переклад якомога точнішим перефразуванням оригінального тексту. Коли є вибір між більш ідіоматичним підходом Lean та більш точним перекладом, я зазвичай обирав останній. Зокрема, будуть місця, де код Lean можна було б "підправити", щоб зробити його більш елегантним та ідіоматичним, але я свідомо уникав цього вибору.

Основні конструкції та результати цього розділу:

Потужність множини
Скінченні та нескінченні множини
Зв'язки з Mathlib-івськіми еквівалентами

Після цього розділу ці нотації будуть вважатися застарілими на користь їхніх еквівалентів із Mathlib.

Підказки від попередніх користувачів

Користувачі супровідного матеріалу, які виконали вправи в цьому розділі, можуть надсилати свої поради майбутнім користувачам цього розділу як PRи.

(Додайте підказку тут)

namespace Chapter3export SetTheory (Set Object nat)variable [SetTheory]

Визначення 3.6.1 (Рівна потужність)

abbrev SetTheory.Set.EqualCard (X Y:Set) : Prop := ∃ f : X → Y, Function.Bijective f

Приклад 3.6.2

theorem SetTheory.Set.Example_3_6_2 : EqualCard {0,1,2} {3,4,5} := byinst✝:SetTheory⊢ {0, 1, 2}.EqualCard {3, 4, 5}
  use open Classical in fun x ↦
    ⟨if x.val = 0 then 3 else if x.val = 1 then 4 else 5, byinst✝:SetTheoryx:{0, 1, 2}.toSubtype⊢ (if ↑x = 0 then 3 else if ↑x = 1 then 4 else 5) ∈ {3, 4, 5} aesopAll goals completed! 🐙⟩
  constructorh.leftinst✝:SetTheory⊢ Function.Injective fun x => ⟨if ↑x = 0 then 3 else if ↑x = 1 then 4 else 5, ⋯⟩h.rightinst✝:SetTheory⊢ Function.Surjective fun x => ⟨if ↑x = 0 then 3 else if ↑x = 1 then 4 else 5, ⋯⟩
  ·h.leftinst✝:SetTheory⊢ Function.Injective fun x => ⟨if ↑x = 0 then 3 else if ↑x = 1 then 4 else 5, ⋯⟩ introh.leftinst✝:SetTheorya₁✝:{0, 1, 2}.toSubtype⊢ ∀ ⦃a₂ : {0, 1, 2}.toSubtype⦄,
  (fun x => ⟨if ↑x = 0 then 3 else if ↑x = 1 then 4 else 5, ⋯⟩) a₁✝ =
      (fun x => ⟨if ↑x = 0 then 3 else if ↑x = 1 then 4 else 5, ⋯⟩) a₂ →
    a₁✝ = a₂; aesopAll goals completed! 🐙
  intro yh.rightinst✝:SetTheoryy:{3, 4, 5}.toSubtype⊢ ∃ a, (fun x => ⟨if ↑x = 0 then 3 else if ↑x = 1 then 4 else 5, ⋯⟩) a = y
  have : y = (3: Object) ∨ y = (4: Object) ∨ y = (5: Object) := byinst✝:SetTheory⊢ {0, 1, 2}.EqualCard {3, 4, 5}
    have := y.propertyinst✝:SetTheoryy:{3, 4, 5}.toSubtypethis:?_mvar.79743 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ ↑y = 3 ∨ ↑y = 4 ∨ ↑y = 5
    aesopAll goals completed! 🐙
  rcases this with (_ | _ | _)h.right.inlinst✝:SetTheoryy:{3, 4, 5}.toSubtypeh✝:↑y = 3⊢ ∃ a, (fun x => ⟨if ↑x = 0 then 3 else if ↑x = 1 then 4 else 5, ⋯⟩) a = yh.right.inr.inlinst✝:SetTheoryy:{3, 4, 5}.toSubtypeh✝:↑y = 4⊢ ∃ a, (fun x => ⟨if ↑x = 0 then 3 else if ↑x = 1 then 4 else 5, ⋯⟩) a = yh.right.inr.inrinst✝:SetTheoryy:{3, 4, 5}.toSubtypeh✝:↑y = 5⊢ ∃ a, (fun x => ⟨if ↑x = 0 then 3 else if ↑x = 1 then 4 else 5, ⋯⟩) a = y
  ·h.right.inlinst✝:SetTheoryy:{3, 4, 5}.toSubtypeh✝:↑y = 3⊢ ∃ a, (fun x => ⟨if ↑x = 0 then 3 else if ↑x = 1 then 4 else 5, ⋯⟩) a = y use ⟨0, byinst✝:SetTheoryy:{3, 4, 5}.toSubtypeh✝:↑y = 3⊢ 0 ∈ {0, 1, 2} simpAll goals completed! 🐙⟩; aesopAll goals completed! 🐙
  ·h.right.inr.inlinst✝:SetTheoryy:{3, 4, 5}.toSubtypeh✝:↑y = 4⊢ ∃ a, (fun x => ⟨if ↑x = 0 then 3 else if ↑x = 1 then 4 else 5, ⋯⟩) a = y use ⟨1, byinst✝:SetTheoryy:{3, 4, 5}.toSubtypeh✝:↑y = 4⊢ 1 ∈ {0, 1, 2} simpAll goals completed! 🐙⟩; aesopAll goals completed! 🐙
  ·h.right.inr.inrinst✝:SetTheoryy:{3, 4, 5}.toSubtypeh✝:↑y = 5⊢ ∃ a, (fun x => ⟨if ↑x = 0 then 3 else if ↑x = 1 then 4 else 5, ⋯⟩) a = y use ⟨2, byinst✝:SetTheoryy:{3, 4, 5}.toSubtypeh✝:↑y = 5⊢ 2 ∈ {0, 1, 2} simpAll goals completed! 🐙⟩; aesopAll goals completed! 🐙

Приклад 3.6.3

theorem declaration uses 'sorry'SetTheory.Set.Example_3_6_3 : EqualCard nat (nat.specify (fun x ↦ Even (x:ℕ))) := byinst✝:SetTheory⊢ nat.EqualCard (nat.specify fun x => Even (nat_equiv.symm x)) sorryAll goals completed! 🐙

@[refl]
theorem declaration uses 'sorry'SetTheory.Set.EqualCard.refl (X:Set) : EqualCard X X := byinst✝:SetTheoryX:Set⊢ X.EqualCard X
  sorryAll goals completed! 🐙

@[symm]
theorem declaration uses 'sorry'SetTheory.Set.EqualCard.symm {X Y:Set} (h: EqualCard X Y) : EqualCard Y X := byinst✝:SetTheoryX:SetY:Seth:X.EqualCard Y⊢ Y.EqualCard X
  sorryAll goals completed! 🐙

@[trans]
theorem declaration uses 'sorry'SetTheory.Set.EqualCard.trans {X Y Z:Set} (h1: EqualCard X Y) (h2: EqualCard Y Z) : EqualCard X Z := byinst✝:SetTheoryX:SetY:SetZ:Seth1:X.EqualCard Yh2:Y.EqualCard Z⊢ X.EqualCard Z
  sorryAll goals completed! 🐙

Твердження 3.6.4 / Вправа 3.6.1

instance SetTheory.Set.EqualCard.inst_setoid : Setoid SetTheory.Set := ⟨ EqualCard, {refl, symm, trans} ⟩

Визначення 3.6.5

abbrev SetTheory.Set.has_card (X:Set) (n:ℕ) : Prop := X ≈ Fin n

theorem SetTheory.Set.has_card_iff (X:Set) (n:ℕ) :
    X.has_card n ↔ ∃ f: X → Fin n, Function.Bijective f := byinst✝:SetTheoryX:Setn:ℕ⊢ X.has_card n ↔ ∃ f, Function.Bijective f
  simp [has_card, HasEquiv.Equiv, Setoid.r, EqualCard]All goals completed! 🐙

Зауваження 3.6.6

theorem declaration uses 'sorry'SetTheory.Set.Remark_3_6_6 (n:ℕ) :
    (nat.specify (fun x ↦ 1 ≤ (x:ℕ) ∧ (x:ℕ) ≤ n)).has_card n := byinst✝:SetTheoryn:ℕ⊢ (nat.specify fun x => 1 ≤ nat_equiv.symm x ∧ nat_equiv.symm x ≤ n).has_card n sorryAll goals completed! 🐙

Приклад 3.6.7

theorem SetTheory.Set.Example_3_6_7a (a:Object) : ({a}:Set).has_card 1 := byinst✝:SetTheorya:Object⊢ {a}.has_card 1
  rw [has_card_iff]inst✝:SetTheorya:Object⊢ ∃ f, Function.Bijective f
  use fun _ ↦ Fin_mk _ 0 (byinst✝:SetTheorya:Objectx✝:{a}.toSubtype⊢ 0 < 1 simpAll goals completed! 🐙)
  constructorh.leftinst✝:SetTheorya:Object⊢ Function.Injective fun x => Fin_mk 1 0 ⋯h.rightinst✝:SetTheorya:Object⊢ Function.Surjective fun x => Fin_mk 1 0 ⋯
  ·h.leftinst✝:SetTheorya:Object⊢ Function.Injective fun x => Fin_mk 1 0 ⋯ intro x1 x2 hfh.leftinst✝:SetTheorya:Objectx1:{a}.toSubtypex2:{a}.toSubtypehf:(fun x => Fin_mk 1 0 ⋯) x1 = (fun x => Fin_mk 1 0 ⋯) x2⊢ x1 = x2; aesopAll goals completed! 🐙
  intro yh.rightinst✝:SetTheorya:Objecty:(Fin 1).toSubtype⊢ ∃ a_1, (fun x => Fin_mk 1 0 ⋯) a_1 = y
  use ⟨a, byinst✝:SetTheorya:Objecty:(Fin 1).toSubtype⊢ a ∈ {a} simpAll goals completed! 🐙⟩
  have := Fin.toNat_lt yhinst✝:SetTheorya:Objecty:(Fin 1).toSubtypethis:?_mvar.134821 := Chapter3.SetTheory.Set.Fin.toNat_lt _fvar.134684⊢ (fun x => Fin_mk 1 0 ⋯) ⟨a, ⋯⟩ = y
  simp_allAll goals completed! 🐙

theorem SetTheory.Set.Example_3_6_7b {a b c d:Object} (hab: a ≠ b) (hac: a ≠ c) (had: a ≠ d)
    (hbc: b ≠ c) (hbd: b ≠ d) (hcd: c ≠ d) : ({a,b,c,d}:Set).has_card 4 := byinst✝:SetTheorya:Objectb:Objectc:Objectd:Objecthab:a ≠ bhac:a ≠ chad:a ≠ dhbc:b ≠ chbd:b ≠ dhcd:c ≠ d⊢ {a, b, c, d}.has_card 4
  rw [has_card_iff]inst✝:SetTheorya:Objectb:Objectc:Objectd:Objecthab:a ≠ bhac:a ≠ chad:a ≠ dhbc:b ≠ chbd:b ≠ dhcd:c ≠ d⊢ ∃ f, Function.Bijective f
  use open Classical in fun x ↦ Fin_mk _ (
    if x.val = a then 0 else if x.val = b then 1 else if x.val = c then 2 else 3
  ) (byinst✝:SetTheorya:Objectb:Objectc:Objectd:Objecthab:a ≠ bhac:a ≠ chad:a ≠ dhbc:b ≠ chbd:b ≠ dhcd:c ≠ dx:{a, b, c, d}.toSubtype⊢ (if ↑x = a then 0 else if ↑x = b then 1 else if ↑x = c then 2 else 3) < 4 aesopAll goals completed! 🐙)
  constructorh.leftinst✝:SetTheorya:Objectb:Objectc:Objectd:Objecthab:a ≠ bhac:a ≠ chad:a ≠ dhbc:b ≠ chbd:b ≠ dhcd:c ≠ d⊢ Function.Injective fun x => Fin_mk 4 (if ↑x = a then 0 else if ↑x = b then 1 else if ↑x = c then 2 else 3) ⋯h.rightinst✝:SetTheorya:Objectb:Objectc:Objectd:Objecthab:a ≠ bhac:a ≠ chad:a ≠ dhbc:b ≠ chbd:b ≠ dhcd:c ≠ d⊢ Function.Surjective fun x => Fin_mk 4 (if ↑x = a then 0 else if ↑x = b then 1 else if ↑x = c then 2 else 3) ⋯
  ·h.leftinst✝:SetTheorya:Objectb:Objectc:Objectd:Objecthab:a ≠ bhac:a ≠ chad:a ≠ dhbc:b ≠ chbd:b ≠ dhcd:c ≠ d⊢ Function.Injective fun x => Fin_mk 4 (if ↑x = a then 0 else if ↑x = b then 1 else if ↑x = c then 2 else 3) ⋯ intro x1 x2 hfh.leftinst✝:SetTheorya:Objectb:Objectc:Objectd:Objecthab:a ≠ bhac:a ≠ chad:a ≠ dhbc:b ≠ chbd:b ≠ dhcd:c ≠ dx1:{a, b, c, d}.toSubtypex2:{a, b, c, d}.toSubtypehf:(fun x => Fin_mk 4 (if ↑x = a then 0 else if ↑x = b then 1 else if ↑x = c then 2 else 3) ⋯) x1 =
  (fun x => Fin_mk 4 (if ↑x = a then 0 else if ↑x = b then 1 else if ↑x = c then 2 else 3) ⋯) x2⊢ x1 = x2; aesopAll goals completed! 🐙
  intro yh.rightinst✝:SetTheorya:Objectb:Objectc:Objectd:Objecthab:a ≠ bhac:a ≠ chad:a ≠ dhbc:b ≠ chbd:b ≠ dhcd:c ≠ dy:(Fin 4).toSubtype⊢ ∃ a_1, (fun x => Fin_mk 4 (if ↑x = a then 0 else if ↑x = b then 1 else if ↑x = c then 2 else 3) ⋯) a_1 = y
  have : y = (0:ℕ) ∨ y = (1:ℕ) ∨ y = (2:ℕ) ∨ y = (3:ℕ) := byinst✝:SetTheorya:Objectb:Objectc:Objectd:Objecthab:a ≠ bhac:a ≠ chad:a ≠ dhbc:b ≠ chbd:b ≠ dhcd:c ≠ d⊢ {a, b, c, d}.has_card 4
    have := Fin.toNat_lt yinst✝:SetTheorya:Objectb:Objectc:Objectd:Objecthab:a ≠ bhac:a ≠ chad:a ≠ dhbc:b ≠ chbd:b ≠ dhcd:c ≠ dy:(Fin 4).toSubtypethis:?_mvar.233132 := Chapter3.SetTheory.Set.Fin.toNat_lt _fvar.215234⊢ ↑y = 0 ∨ ↑y = 1 ∨ ↑y = 2 ∨ ↑y = 3
    omegaAll goals completed! 🐙
  rcases this with (_ | _ | _ | _)h.right.inlinst✝:SetTheorya:Objectb:Objectc:Objectd:Objecthab:a ≠ bhac:a ≠ chad:a ≠ dhbc:b ≠ chbd:b ≠ dhcd:c ≠ dy:(Fin 4).toSubtypeh✝:↑y = 0⊢ ∃ a_1, (fun x => Fin_mk 4 (if ↑x = a then 0 else if ↑x = b then 1 else if ↑x = c then 2 else 3) ⋯) a_1 = yh.right.inr.inlinst✝:SetTheorya:Objectb:Objectc:Objectd:Objecthab:a ≠ bhac:a ≠ chad:a ≠ dhbc:b ≠ chbd:b ≠ dhcd:c ≠ dy:(Fin 4).toSubtypeh✝:↑y = 1⊢ ∃ a_1, (fun x => Fin_mk 4 (if ↑x = a then 0 else if ↑x = b then 1 else if ↑x = c then 2 else 3) ⋯) a_1 = yh.right.inr.inr.inlinst✝:SetTheorya:Objectb:Objectc:Objectd:Objecthab:a ≠ bhac:a ≠ chad:a ≠ dhbc:b ≠ chbd:b ≠ dhcd:c ≠ dy:(Fin 4).toSubtypeh✝:↑y = 2⊢ ∃ a_1, (fun x => Fin_mk 4 (if ↑x = a then 0 else if ↑x = b then 1 else if ↑x = c then 2 else 3) ⋯) a_1 = yh.right.inr.inr.inrinst✝:SetTheorya:Objectb:Objectc:Objectd:Objecthab:a ≠ bhac:a ≠ chad:a ≠ dhbc:b ≠ chbd:b ≠ dhcd:c ≠ dy:(Fin 4).toSubtypeh✝:↑y = 3⊢ ∃ a_1, (fun x => Fin_mk 4 (if ↑x = a then 0 else if ↑x = b then 1 else if ↑x = c then 2 else 3) ⋯) a_1 = y
  ·h.right.inlinst✝:SetTheorya:Objectb:Objectc:Objectd:Objecthab:a ≠ bhac:a ≠ chad:a ≠ dhbc:b ≠ chbd:b ≠ dhcd:c ≠ dy:(Fin 4).toSubtypeh✝:↑y = 0⊢ ∃ a_1, (fun x => Fin_mk 4 (if ↑x = a then 0 else if ↑x = b then 1 else if ↑x = c then 2 else 3) ⋯) a_1 = y use ⟨a, byinst✝:SetTheorya:Objectb:Objectc:Objectd:Objecthab:a ≠ bhac:a ≠ chad:a ≠ dhbc:b ≠ chbd:b ≠ dhcd:c ≠ dy:(Fin 4).toSubtypeh✝:↑y = 0⊢ a ∈ {a, b, c, d} aesopAll goals completed! 🐙⟩; aesopAll goals completed! 🐙
  ·h.right.inr.inlinst✝:SetTheorya:Objectb:Objectc:Objectd:Objecthab:a ≠ bhac:a ≠ chad:a ≠ dhbc:b ≠ chbd:b ≠ dhcd:c ≠ dy:(Fin 4).toSubtypeh✝:↑y = 1⊢ ∃ a_1, (fun x => Fin_mk 4 (if ↑x = a then 0 else if ↑x = b then 1 else if ↑x = c then 2 else 3) ⋯) a_1 = y use ⟨b, byinst✝:SetTheorya:Objectb:Objectc:Objectd:Objecthab:a ≠ bhac:a ≠ chad:a ≠ dhbc:b ≠ chbd:b ≠ dhcd:c ≠ dy:(Fin 4).toSubtypeh✝:↑y = 1⊢ b ∈ {a, b, c, d} aesopAll goals completed! 🐙⟩; aesopAll goals completed! 🐙
  ·h.right.inr.inr.inlinst✝:SetTheorya:Objectb:Objectc:Objectd:Objecthab:a ≠ bhac:a ≠ chad:a ≠ dhbc:b ≠ chbd:b ≠ dhcd:c ≠ dy:(Fin 4).toSubtypeh✝:↑y = 2⊢ ∃ a_1, (fun x => Fin_mk 4 (if ↑x = a then 0 else if ↑x = b then 1 else if ↑x = c then 2 else 3) ⋯) a_1 = y use ⟨c, byinst✝:SetTheorya:Objectb:Objectc:Objectd:Objecthab:a ≠ bhac:a ≠ chad:a ≠ dhbc:b ≠ chbd:b ≠ dhcd:c ≠ dy:(Fin 4).toSubtypeh✝:↑y = 2⊢ c ∈ {a, b, c, d} aesopAll goals completed! 🐙⟩; aesopAll goals completed! 🐙
  ·h.right.inr.inr.inrinst✝:SetTheorya:Objectb:Objectc:Objectd:Objecthab:a ≠ bhac:a ≠ chad:a ≠ dhbc:b ≠ chbd:b ≠ dhcd:c ≠ dy:(Fin 4).toSubtypeh✝:↑y = 3⊢ ∃ a_1, (fun x => Fin_mk 4 (if ↑x = a then 0 else if ↑x = b then 1 else if ↑x = c then 2 else 3) ⋯) a_1 = y use ⟨d, byinst✝:SetTheorya:Objectb:Objectc:Objectd:Objecthab:a ≠ bhac:a ≠ chad:a ≠ dhbc:b ≠ chbd:b ≠ dhcd:c ≠ dy:(Fin 4).toSubtypeh✝:↑y = 3⊢ d ∈ {a, b, c, d} aesopAll goals completed! 🐙⟩; aesopAll goals completed! 🐙

Лема 3.6.9

theorem declaration uses 'sorry'SetTheory.Set.pos_card_nonempty {n:ℕ} (h: n ≥ 1) {X:Set} (hX: X.has_card n) : X ≠ ∅ := byinst✝:SetTheoryn:ℕh:n ≥ 1X:SethX:X.has_card n⊢ X ≠ ∅
  -- цей доказ написан так, щоб співпадати із структурою оригінального тексту.
  by_contra! thisinst✝:SetTheoryn:ℕh:n ≥ 1X:SethX:X.has_card nthis:X = ∅⊢ False
  have hnon : Fin n ≠ ∅ := byinst✝:SetTheoryn:ℕh:n ≥ 1X:SethX:X.has_card n⊢ X ≠ ∅
    apply nonempty_of_inhabited (x := 0)inst✝:SetTheoryn:ℕh:n ≥ 1X:SethX:X.has_card nthis:X = ∅⊢ 0 ∈ Fin n; rw [mem_Fin]inst✝:SetTheoryn:ℕh:n ≥ 1X:SethX:X.has_card nthis:X = ∅⊢ ∃ m < n, 0 = ↑m; use 0, (byinst✝:SetTheoryn:ℕh:n ≥ 1X:SethX:X.has_card nthis:X = ∅⊢ 0 < n omegaAll goals completed! 🐙); rflAll goals completed! 🐙
  rw [has_card_iff] at hXinst✝:SetTheoryn:ℕh:n ≥ 1X:SethX:∃ f, Function.Bijective fthis:X = ∅hnon:Fin n ≠ ∅⊢ False
  choose f hf using hXinst✝:SetTheoryn:ℕh:n ≥ 1X:Setthis:X = ∅hnon:Fin n ≠ ∅f:X.toSubtype → (Fin n).toSubtypehf:Function.Bijective f⊢ False
  sorryAll goals completed! 🐙

-- отримай протиріччя із того факту, що `f` є біекцією
  -- з порожньої множини на непорожню множину

Вправа 3.6.2a

theorem declaration uses 'sorry'SetTheory.Set.has_card_zero {X:Set} : X.has_card 0 ↔ X = ∅ := byinst✝:SetTheoryX:Set⊢ X.has_card 0 ↔ X = ∅ sorryAll goals completed! 🐙

Лема 3.6.9

theorem declaration uses 'sorry'SetTheory.Set.card_erase {n:ℕ} (h: n ≥ 1) {X:Set} (hX: X.has_card n) (x:X) :
    (X \ {x.val}).has_card (n-1) := byinst✝:SetTheoryn:ℕh:n ≥ 1X:SethX:X.has_card nx:X.toSubtype⊢ (X \ {↑x}).has_card (n - 1)
  -- Цей доказ був переписний із оригінального тексту, щоб зробити його
  -- більш дружним для формалізації в Lean
  rw [has_card_iff] at hXinst✝:SetTheoryn:ℕh:n ≥ 1X:SethX:∃ f, Function.Bijective fx:X.toSubtype⊢ (X \ {↑x}).has_card (n - 1); choose f hf using hXinst✝:SetTheoryn:ℕh:n ≥ 1X:Setx:X.toSubtypef:X.toSubtype → (Fin n).toSubtypehf:Function.Bijective f⊢ (X \ {↑x}).has_card (n - 1)
  set X' : Set := X \ {x.val}inst✝:SetTheoryn:ℕh:n ≥ 1X:Setx:X.toSubtypef:X.toSubtype → (Fin n).toSubtypehf:Function.Bijective fX':Chapter3.Set := 
  @sdiff Chapter3.Set Chapter3.SetTheory.Set.instSDiff _fvar.271944
    (@singleton Chapter3.Object Chapter3.Set Chapter3.SetTheory.Set.instSingleton ↑_fvar.271972)⊢ X'.has_card (n - 1)
  set ι : X' → X := fun ⟨y, hy⟩ ↦ ⟨ y, byinst✝:SetTheoryn:ℕh:n ≥ 1X:Setx:X.toSubtypef:X.toSubtype → (Fin n).toSubtypehf:Function.Bijective fX':Chapter3.Set := 
  @sdiff Chapter3.Set Chapter3.SetTheory.Set.instSDiff _fvar.271944
    (@singleton Chapter3.Object Chapter3.Set Chapter3.SetTheory.Set.instSingleton ↑_fvar.271972)x✝:X'.toSubtypey:Objecthy:y ∈ X'⊢ y ∈ X aesopAll goals completed! 🐙 ⟩
  observe hι : ∀ x:X', (ι x:Object) = xinst✝:SetTheoryn:ℕh:n ≥ 1X:Setx:X.toSubtypef:X.toSubtype → (Fin n).toSubtypehf:Function.Bijective fX':Chapter3.Set := 
  @sdiff Chapter3.Set Chapter3.SetTheory.Set.instSDiff _fvar.271944
    (@singleton Chapter3.Object Chapter3.Set Chapter3.SetTheory.Set.instSingleton ↑_fvar.271972)ι:Chapter3.SetTheory.Set.toSubtype _fvar.272097 → Chapter3.SetTheory.Set.toSubtype _fvar.271944 := 
  fun x =>
    match x with
    | ⟨y, hy⟩ => ⟨y, ⋯⟩hι:∀ (a : X'.toSubtype), ↑(ι a) = ↑a⊢ X'.has_card (n - 1)
  choose m₀ hm₀ hm₀f using (mem_Fin _ _).mp (f x).propertyinst✝:SetTheoryn:ℕh:n ≥ 1X:Setx:X.toSubtypef:X.toSubtype → (Fin n).toSubtypehf:Function.Bijective fX':Chapter3.Set := 
  @sdiff Chapter3.Set Chapter3.SetTheory.Set.instSDiff _fvar.271944
    (@singleton Chapter3.Object Chapter3.Set Chapter3.SetTheory.Set.instSingleton ↑_fvar.271972)ι:Chapter3.SetTheory.Set.toSubtype _fvar.272097 → Chapter3.SetTheory.Set.toSubtype _fvar.271944 := 
  fun x =>
    match x with
    | ⟨y, hy⟩ => ⟨y, ⋯⟩hι:∀ (a : X'.toSubtype), ↑(ι a) = ↑am₀:ℕhm₀:m₀ < nhm₀f:↑(f x) = ↑m₀⊢ X'.has_card (n - 1)
  set g : X' → Fin (n-1) := fun x' ↦
    let := Fin.toNat_lt (f (ι x'))
    let : (f (ι x'):ℕ) ≠ m₀ := byinst✝:SetTheoryn:ℕh:n ≥ 1X:Setx:X.toSubtypef:X.toSubtype → (Fin n).toSubtypehf:Function.Bijective fX':Chapter3.Set := 
  @sdiff Chapter3.Set Chapter3.SetTheory.Set.instSDiff _fvar.271944
    (@singleton Chapter3.Object Chapter3.Set Chapter3.SetTheory.Set.instSingleton ↑_fvar.271972)ι:Chapter3.SetTheory.Set.toSubtype _fvar.272097 → Chapter3.SetTheory.Set.toSubtype _fvar.271944 := 
  fun x =>
    match x with
    | ⟨y, hy⟩ => ⟨y, ⋯⟩hι:∀ (a : X'.toSubtype), ↑(ι a) = ↑am₀:ℕhm₀:m₀ < nhm₀f:↑(f x) = ↑m₀x':X'.toSubtypethis:↑(@_fvar.271986 (@_fvar.274488 _fvar.275348)) < _fvar.271942 := Chapter3.SetTheory.Set.Fin.toNat_lt (@_fvar.271986 (@_fvar.274488 _fvar.275348))⊢ ↑(f (ι x')) ≠ m₀
      by_contra!inst✝:SetTheoryn:ℕh:n ≥ 1X:Setx:X.toSubtypef:X.toSubtype → (Fin n).toSubtypehf:Function.Bijective fX':Chapter3.Set := 
  @sdiff Chapter3.Set Chapter3.SetTheory.Set.instSDiff _fvar.271944
    (@singleton Chapter3.Object Chapter3.Set Chapter3.SetTheory.Set.instSingleton ↑_fvar.271972)ι:Chapter3.SetTheory.Set.toSubtype _fvar.272097 → Chapter3.SetTheory.Set.toSubtype _fvar.271944 := 
  fun x =>
    match x with
    | ⟨y, hy⟩ => ⟨y, ⋯⟩hι:∀ (a : X'.toSubtype), ↑(ι a) = ↑am₀:ℕhm₀:m₀ < nhm₀f:↑(f x) = ↑m₀x':X'.toSubtypethis✝:↑(@_fvar.271986 (@_fvar.274488 _fvar.275348)) < _fvar.271942 := Chapter3.SetTheory.Set.Fin.toNat_lt (@_fvar.271986 (@_fvar.274488 _fvar.275348))this:↑(f (ι x')) = m₀⊢ False; simp [←this, Subtype.val_inj, hf.1.eq_iff, ι] at hm₀finst✝:SetTheoryn:ℕh:n ≥ 1X:Setx:X.toSubtypef:X.toSubtype → (Fin n).toSubtypehf:Function.Bijective fX':Chapter3.Set := 
  @sdiff Chapter3.Set Chapter3.SetTheory.Set.instSDiff _fvar.271944
    (@singleton Chapter3.Object Chapter3.Set Chapter3.SetTheory.Set.instSingleton ↑_fvar.271972)ι:Chapter3.SetTheory.Set.toSubtype _fvar.272097 → Chapter3.SetTheory.Set.toSubtype _fvar.271944 := 
  fun x =>
    match x with
    | ⟨y, hy⟩ => ⟨y, ⋯⟩hι:∀ (a : X'.toSubtype), ↑(ι a) = ↑am₀:ℕhm₀:m₀ < nx':X'.toSubtypethis✝:↑(@_fvar.271986 (@_fvar.274488 _fvar.275348)) < _fvar.271942 := Chapter3.SetTheory.Set.Fin.toNat_lt (@_fvar.271986 (@_fvar.274488 _fvar.275348))this:↑(f (ι x')) = m₀hm₀f:x = ⟨↑x', ⋯⟩⊢ False
      have := x'.propertyinst✝:SetTheoryn:ℕh:n ≥ 1X:Setx:X.toSubtypef:X.toSubtype → (Fin n).toSubtypehf:Function.Bijective fX':Chapter3.Set := 
  @sdiff Chapter3.Set Chapter3.SetTheory.Set.instSDiff _fvar.271944
    (@singleton Chapter3.Object Chapter3.Set Chapter3.SetTheory.Set.instSingleton ↑_fvar.271972)ι:Chapter3.SetTheory.Set.toSubtype _fvar.272097 → Chapter3.SetTheory.Set.toSubtype _fvar.271944 := 
  fun x =>
    match x with
    | ⟨y, hy⟩ => ⟨y, ⋯⟩hι:∀ (a : X'.toSubtype), ↑(ι a) = ↑am₀:ℕhm₀:m₀ < nx':X'.toSubtypethis✝¹:↑(@_fvar.271986 (@_fvar.274488 _fvar.275348)) < _fvar.271942 := Chapter3.SetTheory.Set.Fin.toNat_lt (@_fvar.271986 (@_fvar.274488 _fvar.275348))this✝:↑(f (ι x')) = m₀hm₀f:x = ⟨↑x', ⋯⟩this:?_mvar.282467 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ False; aesopAll goals completed! 🐙
    if h' : f (ι x') < m₀ then Fin_mk _ (f (ι x')) (byinst✝:SetTheoryn:ℕh:n ≥ 1X:Setx:X.toSubtypef:X.toSubtype → (Fin n).toSubtypehf:Function.Bijective fX':Chapter3.Set := 
  @sdiff Chapter3.Set Chapter3.SetTheory.Set.instSDiff _fvar.271944
    (@singleton Chapter3.Object Chapter3.Set Chapter3.SetTheory.Set.instSingleton ↑_fvar.271972)ι:Chapter3.SetTheory.Set.toSubtype _fvar.272097 → Chapter3.SetTheory.Set.toSubtype _fvar.271944 := 
  fun x =>
    match x with
    | ⟨y, hy⟩ => ⟨y, ⋯⟩hι:∀ (a : X'.toSubtype), ↑(ι a) = ↑am₀:ℕhm₀:m₀ < nhm₀f:↑(f x) = ↑m₀x':X'.toSubtypethis✝:↑(@_fvar.271986 (@_fvar.274488 _fvar.275348)) < _fvar.271942 := Chapter3.SetTheory.Set.Fin.toNat_lt (@_fvar.271986 (@_fvar.274488 _fvar.275348))this:↑(@_fvar.271986 (@_fvar.274488 _fvar.275348)) ≠ _fvar.275218 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)h':↑(f (ι x')) < m₀⊢ ↑(f (ι x')) < n - 1 omegaAll goals completed! 🐙)
    else Fin_mk _ (f (ι x') - 1) (byinst✝:SetTheoryn:ℕh:n ≥ 1X:Setx:X.toSubtypef:X.toSubtype → (Fin n).toSubtypehf:Function.Bijective fX':Chapter3.Set := 
  @sdiff Chapter3.Set Chapter3.SetTheory.Set.instSDiff _fvar.271944
    (@singleton Chapter3.Object Chapter3.Set Chapter3.SetTheory.Set.instSingleton ↑_fvar.271972)ι:Chapter3.SetTheory.Set.toSubtype _fvar.272097 → Chapter3.SetTheory.Set.toSubtype _fvar.271944 := 
  fun x =>
    match x with
    | ⟨y, hy⟩ => ⟨y, ⋯⟩hι:∀ (a : X'.toSubtype), ↑(ι a) = ↑am₀:ℕhm₀:m₀ < nhm₀f:↑(f x) = ↑m₀x':X'.toSubtypethis✝:↑(@_fvar.271986 (@_fvar.274488 _fvar.275348)) < _fvar.271942 := Chapter3.SetTheory.Set.Fin.toNat_lt (@_fvar.271986 (@_fvar.274488 _fvar.275348))this:↑(@_fvar.271986 (@_fvar.274488 _fvar.275348)) ≠ _fvar.275218 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)h':¬↑(f (ι x')) < m₀⊢ ↑(f (ι x')) - 1 < n - 1 omegaAll goals completed! 🐙)
  have hg_def (x':X') : if (f (ι x'):ℕ) < m₀ then (g x':ℕ) = f (ι x') else (g x':ℕ) = f (ι x') - 1 := byinst✝:SetTheoryn:ℕh:n ≥ 1X:SethX:X.has_card nx:X.toSubtype⊢ (X \ {↑x}).has_card (n - 1)
    split_ifs with h'pos._@._hyg.2592inst✝:SetTheoryn:ℕh:n ≥ 1X:Setx:X.toSubtypef:X.toSubtype → (Fin n).toSubtypehf:Function.Bijective fX':Chapter3.Set := 
  @sdiff Chapter3.Set Chapter3.SetTheory.Set.instSDiff _fvar.271944
    (@singleton Chapter3.Object Chapter3.Set Chapter3.SetTheory.Set.instSingleton ↑_fvar.271972)ι:Chapter3.SetTheory.Set.toSubtype _fvar.272097 → Chapter3.SetTheory.Set.toSubtype _fvar.271944 := 
  fun x =>
    match x with
    | ⟨y, hy⟩ => ⟨y, ⋯⟩hι:∀ (a : X'.toSubtype), ↑(ι a) = ↑am₀:ℕhm₀:m₀ < nhm₀f:↑(f x) = ↑m₀g:Chapter3.SetTheory.Set.toSubtype _fvar.272097 → (Chapter3.SetTheory.Set.Fin (_fvar.271942 - 1)).toSubtype := 
  fun x' =>
    let this := ⋯;
    let this := ⋯;
    if h' : ↑(@_fvar.271986 (@_fvar.274488 x')) < _fvar.275218 then
      Chapter3.SetTheory.Set.Fin_mk (_fvar.271942 - 1) ↑(@_fvar.271986 (@_fvar.274488 x')) ⋯
    else Chapter3.SetTheory.Set.Fin_mk (_fvar.271942 - 1) (↑(@_fvar.271986 (@_fvar.274488 x')) - 1) ⋯x':X'.toSubtypeh':↑(f (ι x')) < m₀⊢ ↑(g x') = ↑(f (ι x'))neg._@._hyg.2592inst✝:SetTheoryn:ℕh:n ≥ 1X:Setx:X.toSubtypef:X.toSubtype → (Fin n).toSubtypehf:Function.Bijective fX':Chapter3.Set := 
  @sdiff Chapter3.Set Chapter3.SetTheory.Set.instSDiff _fvar.271944
    (@singleton Chapter3.Object Chapter3.Set Chapter3.SetTheory.Set.instSingleton ↑_fvar.271972)ι:Chapter3.SetTheory.Set.toSubtype _fvar.272097 → Chapter3.SetTheory.Set.toSubtype _fvar.271944 := 
  fun x =>
    match x with
    | ⟨y, hy⟩ => ⟨y, ⋯⟩hι:∀ (a : X'.toSubtype), ↑(ι a) = ↑am₀:ℕhm₀:m₀ < nhm₀f:↑(f x) = ↑m₀g:Chapter3.SetTheory.Set.toSubtype _fvar.272097 → (Chapter3.SetTheory.Set.Fin (_fvar.271942 - 1)).toSubtype := 
  fun x' =>
    let this := ⋯;
    let this := ⋯;
    if h' : ↑(@_fvar.271986 (@_fvar.274488 x')) < _fvar.275218 then
      Chapter3.SetTheory.Set.Fin_mk (_fvar.271942 - 1) ↑(@_fvar.271986 (@_fvar.274488 x')) ⋯
    else Chapter3.SetTheory.Set.Fin_mk (_fvar.271942 - 1) (↑(@_fvar.271986 (@_fvar.274488 x')) - 1) ⋯x':X'.toSubtypeh':¬↑(f (ι x')) < m₀⊢ ↑(g x') = ↑(f (ι x')) - 1 <;>pos._@._hyg.2592inst✝:SetTheoryn:ℕh:n ≥ 1X:Setx:X.toSubtypef:X.toSubtype → (Fin n).toSubtypehf:Function.Bijective fX':Chapter3.Set := 
  @sdiff Chapter3.Set Chapter3.SetTheory.Set.instSDiff _fvar.271944
    (@singleton Chapter3.Object Chapter3.Set Chapter3.SetTheory.Set.instSingleton ↑_fvar.271972)ι:Chapter3.SetTheory.Set.toSubtype _fvar.272097 → Chapter3.SetTheory.Set.toSubtype _fvar.271944 := 
  fun x =>
    match x with
    | ⟨y, hy⟩ => ⟨y, ⋯⟩hι:∀ (a : X'.toSubtype), ↑(ι a) = ↑am₀:ℕhm₀:m₀ < nhm₀f:↑(f x) = ↑m₀g:Chapter3.SetTheory.Set.toSubtype _fvar.272097 → (Chapter3.SetTheory.Set.Fin (_fvar.271942 - 1)).toSubtype := 
  fun x' =>
    let this := ⋯;
    let this := ⋯;
    if h' : ↑(@_fvar.271986 (@_fvar.274488 x')) < _fvar.275218 then
      Chapter3.SetTheory.Set.Fin_mk (_fvar.271942 - 1) ↑(@_fvar.271986 (@_fvar.274488 x')) ⋯
    else Chapter3.SetTheory.Set.Fin_mk (_fvar.271942 - 1) (↑(@_fvar.271986 (@_fvar.274488 x')) - 1) ⋯x':X'.toSubtypeh':↑(f (ι x')) < m₀⊢ ↑(g x') = ↑(f (ι x'))neg._@._hyg.2592inst✝:SetTheoryn:ℕh:n ≥ 1X:Setx:X.toSubtypef:X.toSubtype → (Fin n).toSubtypehf:Function.Bijective fX':Chapter3.Set := 
  @sdiff Chapter3.Set Chapter3.SetTheory.Set.instSDiff _fvar.271944
    (@singleton Chapter3.Object Chapter3.Set Chapter3.SetTheory.Set.instSingleton ↑_fvar.271972)ι:Chapter3.SetTheory.Set.toSubtype _fvar.272097 → Chapter3.SetTheory.Set.toSubtype _fvar.271944 := 
  fun x =>
    match x with
    | ⟨y, hy⟩ => ⟨y, ⋯⟩hι:∀ (a : X'.toSubtype), ↑(ι a) = ↑am₀:ℕhm₀:m₀ < nhm₀f:↑(f x) = ↑m₀g:Chapter3.SetTheory.Set.toSubtype _fvar.272097 → (Chapter3.SetTheory.Set.Fin (_fvar.271942 - 1)).toSubtype := 
  fun x' =>
    let this := ⋯;
    let this := ⋯;
    if h' : ↑(@_fvar.271986 (@_fvar.274488 x')) < _fvar.275218 then
      Chapter3.SetTheory.Set.Fin_mk (_fvar.271942 - 1) ↑(@_fvar.271986 (@_fvar.274488 x')) ⋯
    else Chapter3.SetTheory.Set.Fin_mk (_fvar.271942 - 1) (↑(@_fvar.271986 (@_fvar.274488 x')) - 1) ⋯x':X'.toSubtypeh':¬↑(f (ι x')) < m₀⊢ ↑(g x') = ↑(f (ι x')) - 1 simp [g,h']All goals completed! 🐙
  have hg : Function.Bijective g := byinst✝:SetTheoryn:ℕh:n ≥ 1X:SethX:X.has_card nx:X.toSubtype⊢ (X \ {↑x}).has_card (n - 1) sorryAll goals completed! 🐙
  use gAll goals completed! 🐙

Твердження 3.6.8 (Унікальність потужності)

theorem SetTheory.Set.card_uniq {X:Set} {n m:ℕ} (h1: X.has_card n) (h2: X.has_card m) : n = m := byinst✝:SetTheoryX:Setn:ℕm:ℕh1:X.has_card nh2:X.has_card m⊢ n = m
  -- цей доказ написан так, щоб співпадати із структурою оригінального тексту.
  revert X minst✝:SetTheoryn:ℕ⊢ ∀ {X : Set} {m : ℕ}, X.has_card n → X.has_card m → n = m; induction' n with n hnzeroinst✝:SetTheory⊢ ∀ {X : Set} {m : ℕ}, X.has_card 0 → X.has_card m → 0 = msuccinst✝:SetTheoryn:ℕhn:∀ {X : Set} {m : ℕ}, X.has_card n → X.has_card m → n = m⊢ ∀ {X : Set} {m : ℕ}, X.has_card (n + 1) → X.has_card m → n + 1 = m
  .zeroinst✝:SetTheory⊢ ∀ {X : Set} {m : ℕ}, X.has_card 0 → X.has_card m → 0 = m intro _ _ h1 h2zeroinst✝:SetTheoryX✝:Setm✝:ℕh1:X✝.has_card 0h2:X✝.has_card m✝⊢ 0 = m✝; rw [has_card_zero] at h1zeroinst✝:SetTheoryX✝:Setm✝:ℕh1:X✝ = ∅h2:X✝.has_card m✝⊢ 0 = m✝; contrapose! h1zeroinst✝:SetTheoryX✝:Setm✝:ℕh2:X✝.has_card m✝h1:0 ≠ m✝⊢ X✝ ≠ ∅
    apply pos_card_nonempty _ h2inst✝:SetTheoryX✝:Setm✝:ℕh2:X✝.has_card m✝h1:0 ≠ m✝⊢ m✝ ≥ 1; omegaAll goals completed! 🐙
  intro X m h1 h2succinst✝:SetTheoryn:ℕhn:∀ {X : Set} {m : ℕ}, X.has_card n → X.has_card m → n = mX:Setm:ℕh1:X.has_card (n + 1)h2:X.has_card m⊢ n + 1 = m
  have : X ≠ ∅ := pos_card_nonempty (byinst✝:SetTheoryn:ℕhn:∀ {X : Set} {m : ℕ}, X.has_card n → X.has_card m → n = mX:Setm:ℕh1:X.has_card (n + 1)h2:X.has_card m⊢ n + 1 ≥ 1 omegaAll goals completed! 🐙) h1
  choose x hx using nonempty_def thissuccinst✝:SetTheoryn:ℕhn:∀ {X : Set} {m : ℕ}, X.has_card n → X.has_card m → n = mX:Setm:ℕh1:X.has_card (n + 1)h2:X.has_card mthis:_fvar.301234 ≠ ∅ := Chapter3.SetTheory.Set.pos_card_nonempty ?_mvar.301360 _fvar.301240x:Objecthx:x ∈ X⊢ n + 1 = m
  have : m ≠ 0 := byinst✝:SetTheoryX:Setn:ℕm:ℕh1:X.has_card nh2:X.has_card m⊢ n = m contrapose! thisinst✝:SetTheoryn:ℕhn:∀ {X : Set} {m : ℕ}, X.has_card n → X.has_card m → n = mX:Setm:ℕh1:X.has_card (n + 1)h2:X.has_card mx:Objecthx:x ∈ Xthis:m = 0⊢ X = ∅; simpa [has_card_zero, this] using h2All goals completed! 🐙
  specialize hn (card_erase ?_ h1 ⟨ _, hx ⟩) (card_erase ?_ h2 ⟨ _, hx ⟩)succ.specialize_1inst✝:SetTheoryn:ℕhn:∀ {X : Set} {m : ℕ}, X.has_card n → X.has_card m → n = mX:Setm:ℕh1:X.has_card (n + 1)h2:X.has_card mthis✝:_fvar.301234 ≠ ∅ := Chapter3.SetTheory.Set.pos_card_nonempty ?_mvar.301360 _fvar.301240x:Objecthx:x ∈ Xthis:_fvar.301237 ≠ 0 := ?_mvar.301519⊢ n + 1 ≥ 1succ.specialize_2inst✝:SetTheoryn:ℕhn:∀ {X : Set} {m : ℕ}, X.has_card n → X.has_card m → n = mX:Setm:ℕh1:X.has_card (n + 1)h2:X.has_card mthis✝:_fvar.301234 ≠ ∅ := Chapter3.SetTheory.Set.pos_card_nonempty ?_mvar.301360 _fvar.301240x:Objecthx:x ∈ Xthis:_fvar.301237 ≠ 0 := ?_mvar.301519⊢ m ≥ 1succinst✝:SetTheoryn:ℕX:Setm:ℕh1:X.has_card (n + 1)h2:X.has_card mthis✝:_fvar.301234 ≠ ∅ := Chapter3.SetTheory.Set.pos_card_nonempty ?_mvar.301360 _fvar.301240x:Objecthx:x ∈ Xthis:_fvar.301237 ≠ 0 := ?_mvar.301519hn:n = m - 1⊢ n + 1 = m <;>succ.specialize_1inst✝:SetTheoryn:ℕhn:∀ {X : Set} {m : ℕ}, X.has_card n → X.has_card m → n = mX:Setm:ℕh1:X.has_card (n + 1)h2:X.has_card mthis✝:_fvar.301234 ≠ ∅ := Chapter3.SetTheory.Set.pos_card_nonempty ?_mvar.301360 _fvar.301240x:Objecthx:x ∈ Xthis:_fvar.301237 ≠ 0 := ?_mvar.301519⊢ n + 1 ≥ 1succ.specialize_2inst✝:SetTheoryn:ℕhn:∀ {X : Set} {m : ℕ}, X.has_card n → X.has_card m → n = mX:Setm:ℕh1:X.has_card (n + 1)h2:X.has_card mthis✝:_fvar.301234 ≠ ∅ := Chapter3.SetTheory.Set.pos_card_nonempty ?_mvar.301360 _fvar.301240x:Objecthx:x ∈ Xthis:_fvar.301237 ≠ 0 := ?_mvar.301519⊢ m ≥ 1succinst✝:SetTheoryn:ℕX:Setm:ℕh1:X.has_card (n + 1)h2:X.has_card mthis✝:_fvar.301234 ≠ ∅ := Chapter3.SetTheory.Set.pos_card_nonempty ?_mvar.301360 _fvar.301240x:Objecthx:x ∈ Xthis:_fvar.301237 ≠ 0 := ?_mvar.301519hn:n = m - 1⊢ n + 1 = m omegaAll goals completed! 🐙

lemma SetTheory.Set.Example_3_6_8_a: ({0,1,2}:Set).has_card 3 := byinst✝:SetTheory⊢ {0, 1, 2}.has_card 3
  rw [has_card_iff]inst✝:SetTheory⊢ ∃ f, Function.Bijective f
  have : ({0, 1, 2}: Set) = SetTheory.Set.Fin 3 := byinst✝:SetTheory⊢ {0, 1, 2}.has_card 3
    ext xhinst✝:SetTheoryx:Object⊢ x ∈ {0, 1, 2} ↔ x ∈ Fin 3
    simp only [mem_insert, mem_singleton, mem_Fin]hinst✝:SetTheoryx:Object⊢ x = 0 ∨ x = 1 ∨ x = 2 ↔ ∃ m < 3, x = ↑m
    constructorh.mpinst✝:SetTheoryx:Object⊢ x = 0 ∨ x = 1 ∨ x = 2 → ∃ m < 3, x = ↑mh.mprinst✝:SetTheoryx:Object⊢ (∃ m < 3, x = ↑m) → x = 0 ∨ x = 1 ∨ x = 2
    ·h.mpinst✝:SetTheoryx:Object⊢ x = 0 ∨ x = 1 ∨ x = 2 → ∃ m < 3, x = ↑m aesopAll goals completed! 🐙
    rintro ⟨x, ⟨_, rfl⟩⟩h.mpr.intro.introinst✝:SetTheoryx:ℕleft✝:x < 3⊢ ↑x = 0 ∨ ↑x = 1 ∨ ↑x = 2
    simp only [nat_coe_eq_iff]h.mpr.intro.introinst✝:SetTheoryx:ℕleft✝:x < 3⊢ x = 0 ∨ x = 1 ∨ x = 2
    omegaAll goals completed! 🐙
  rw [this]inst✝:SetTheorythis:{0, 1, 2} = Chapter3.SetTheory.Set.Fin 3 := ?_mvar.302860⊢ ∃ f, Function.Bijective f
  use idhinst✝:SetTheorythis:{0, 1, 2} = Chapter3.SetTheory.Set.Fin 3 := ?_mvar.302860⊢ Function.Bijective id
  exact Function.bijective_idAll goals completed! 🐙

lemma SetTheory.Set.Example_3_6_8_b: ({3,4}:Set).has_card 2 := byinst✝:SetTheory⊢ {3, 4}.has_card 2
  rw [has_card_iff]inst✝:SetTheory⊢ ∃ f, Function.Bijective f
  use open Classical in fun x ↦ Fin_mk _ (if x = (3:Object) then 0 else 1) (byinst✝:SetTheoryx:{3, 4}.toSubtype⊢ (if ↑x = 3 then 0 else 1) < 2 aesopAll goals completed! 🐙)
  constructorh.leftinst✝:SetTheory⊢ Function.Injective fun x => Fin_mk 2 (if ↑x = 3 then 0 else 1) ⋯h.rightinst✝:SetTheory⊢ Function.Surjective fun x => Fin_mk 2 (if ↑x = 3 then 0 else 1) ⋯
  ·h.leftinst✝:SetTheory⊢ Function.Injective fun x => Fin_mk 2 (if ↑x = 3 then 0 else 1) ⋯ intro x1 x2h.leftinst✝:SetTheoryx1:{3, 4}.toSubtypex2:{3, 4}.toSubtype⊢ (fun x => Fin_mk 2 (if ↑x = 3 then 0 else 1) ⋯) x1 = (fun x => Fin_mk 2 (if ↑x = 3 then 0 else 1) ⋯) x2 → x1 = x2
    aesopAll goals completed! 🐙
  intro yh.rightinst✝:SetTheoryy:(Fin 2).toSubtype⊢ ∃ a, (fun x => Fin_mk 2 (if ↑x = 3 then 0 else 1) ⋯) a = y
  have := Fin.toNat_lt yh.rightinst✝:SetTheoryy:(Fin 2).toSubtypethis:?_mvar.328400 := Chapter3.SetTheory.Set.Fin.toNat_lt _fvar.328396⊢ ∃ a, (fun x => Fin_mk 2 (if ↑x = 3 then 0 else 1) ⋯) a = y
  have : y = (0:ℕ) ∨ y = (1:ℕ) := byinst✝:SetTheory⊢ {3, 4}.has_card 2 omegaAll goals completed! 🐙
  aesopAll goals completed! 🐙

lemma SetTheory.Set.Example_3_6_8_c : ¬({0,1,2}:Set) ≈ ({3,4}:Set) := byinst✝:SetTheory⊢ ¬{0, 1, 2} ≈ {3, 4}
  by_contra hinst✝:SetTheoryh:{0, 1, 2} ≈ {3, 4}⊢ False
  have h1 : Fin 3 ≈ Fin 2 := (Example_3_6_8_a.symm.trans h).trans Example_3_6_8_binst✝:SetTheoryh:{0, 1, 2} ≈ {3, 4}h1:Chapter3.SetTheory.Set.Fin 3 ≈ Chapter3.SetTheory.Set.Fin 2 := 
  Chapter3.SetTheory.Set.EqualCard.trans
    (Chapter3.SetTheory.Set.EqualCard.trans (Chapter3.SetTheory.Set.EqualCard.symm Chapter3.SetTheory.Set.Example_3_6_8_a)
      _fvar.373641)
    Chapter3.SetTheory.Set.Example_3_6_8_b⊢ False
  have h2 : Fin 3 ≈ Fin 3 := byinst✝:SetTheory⊢ ¬{0, 1, 2} ≈ {3, 4} rflAll goals completed! 🐙
  have := card_uniq h1 h2inst✝:SetTheoryh:{0, 1, 2} ≈ {3, 4}h1:Chapter3.SetTheory.Set.Fin 3 ≈ Chapter3.SetTheory.Set.Fin 2 := 
  Chapter3.SetTheory.Set.EqualCard.trans
    (Chapter3.SetTheory.Set.EqualCard.trans (Chapter3.SetTheory.Set.EqualCard.symm Chapter3.SetTheory.Set.Example_3_6_8_a)
      _fvar.373641)
    Chapter3.SetTheory.Set.Example_3_6_8_bh2:Chapter3.SetTheory.Set.Fin 3 ≈ Chapter3.SetTheory.Set.Fin 3 := ?_mvar.373795this:?_mvar.373823 := Chapter3.SetTheory.Set.card_uniq _fvar.373755 _fvar.373796⊢ False
  contradictionAll goals completed! 🐙

abbrev SetTheory.Set.finite (X:Set) : Prop := ∃ n:ℕ, X.has_card nabbrev SetTheory.Set.infinite (X:Set) : Prop := ¬ finite X

Вправа 3.6.3, сформульовано з використанням натуральних чисел Mathlib

theorem declaration uses 'sorry'SetTheory.Set.bounded_on_finite {n:ℕ} (f: Fin n → nat) : ∃ M, ∀ i, (f i:ℕ) ≤ M := byinst✝:SetTheoryn:ℕf:(Fin n).toSubtype → nat.toSubtype⊢ ∃ M, ∀ (i : (Fin n).toSubtype), nat_equiv.symm (f i) ≤ M sorryAll goals completed! 🐙

Теорема 3.6.12

theorem SetTheory.Set.nat_infinite : infinite nat := byinst✝:SetTheory⊢ nat.infinite
  -- цей доказ написан так, щоб співпадати із структурою оригінального тексту.
  by_contra thisinst✝:SetTheorythis:nat.finite⊢ False; choose n hn using thisinst✝:SetTheoryn:ℕhn:nat.has_card n⊢ False
  simp [has_card] at hninst✝:SetTheoryn:ℕhn:nat ≈ Fin n⊢ False; symm at hninst✝:SetTheoryn:ℕhn:Fin n ≈ nat⊢ False; simp [HasEquiv.Equiv, Setoid.r, EqualCard] at hninst✝:SetTheoryn:ℕhn:∃ f, Function.Bijective f⊢ False
  choose f hf using hninst✝:SetTheoryn:ℕf:(Fin n).toSubtype → nat.toSubtypehf:Function.Bijective f⊢ False; choose M hM using bounded_on_finite finst✝:SetTheoryn:ℕf:(Fin n).toSubtype → nat.toSubtypehf:Function.Bijective fM:ℕhM:∀ (i : (Fin n).toSubtype), nat_equiv.symm (f i) ≤ M⊢ False
  replace hf := hf.surjective ↑(M+1)inst✝:SetTheoryn:ℕf:(Fin n).toSubtype → nat.toSubtypeM:ℕhM:∀ (i : (Fin n).toSubtype), nat_equiv.symm (f i) ≤ Mhf:?_mvar.381182 := Function.Bijective.surjective _fvar.381158 ↑(_fvar.381174 + 1)⊢ False; contrapose! hfinst✝:SetTheoryn:ℕf:(Fin n).toSubtype → nat.toSubtypeM:ℕhM:∀ (i : (Fin n).toSubtype), nat_equiv.symm (f i) ≤ Mhf:¬False⊢ ∀ (a : (Fin n).toSubtype), f a ≠ ↑(M + 1)
  peel hM with hihinst✝:SetTheoryn:ℕf:(Fin n).toSubtype → nat.toSubtypeM:ℕhM:∀ (i : (Fin n).toSubtype), nat_equiv.symm (f i) ≤ Mhf:¬Falsea✝:(Fin n).toSubtypehi:nat_equiv.symm (f a✝) ≤ M⊢ f a✝ ≠ ↑(M + 1); contrapose! hihinst✝:SetTheoryn:ℕf:(Fin n).toSubtype → nat.toSubtypeM:ℕhM:∀ (i : (Fin n).toSubtype), nat_equiv.symm (f i) ≤ Mhf:¬Falsea✝:(Fin n).toSubtypehi:f a✝ = ↑(M + 1)⊢ M < nat_equiv.symm (f a✝)
  apply_fun nat_equiv.symm at hihinst✝:SetTheoryn:ℕf:(Fin n).toSubtype → nat.toSubtypeM:ℕhM:∀ (i : (Fin n).toSubtype), nat_equiv.symm (f i) ≤ Mhf:¬Falsea✝:(Fin n).toSubtypehi:nat_equiv.symm (f a✝) = nat_equiv.symm ↑(M + 1)⊢ M < nat_equiv.symm (f a✝); simp_allAll goals completed! 🐙

open Classical in
/-- Для цілей Lean зручно надавати нескінченним множинам ``сміттєву`` потужність як нуль. -/
noncomputable def SetTheory.Set.card (X:Set) : ℕ := if h:X.finite then h.choose else 0

theorem SetTheory.Set.has_card_card {X:Set} (hX: X.finite) : X.has_card (SetTheory.Set.card X) := byinst✝:SetTheoryX:SethX:X.finite⊢ X.has_card X.card
  simp [card, hX, hX.choose_spec]All goals completed! 🐙

theorem SetTheory.Set.has_card_to_card {X:Set} {n: ℕ}: X.has_card n → X.card = n := byinst✝:SetTheoryX:Setn:ℕ⊢ X.has_card n → X.card = n
  intro hinst✝:SetTheoryX:Setn:ℕh:X.has_card n⊢ X.card = n; simp [card, card_uniq (⟨ n, h ⟩:X.finite).choose_spec h]inst✝:SetTheoryX:Setn:ℕh:X.has_card n⊢ (∀ (x : ℕ), ¬X.has_card x) → 0 = n; aesopAll goals completed! 🐙

theorem SetTheory.Set.card_to_has_card {X:Set} {n: ℕ} (hn: n ≠ 0): X.card = n → X.has_card n
  := byinst✝:SetTheoryX:Setn:ℕhn:n ≠ 0⊢ X.card = n → X.has_card n grind [card, has_card_card]All goals completed! 🐙

theorem SetTheory.Set.card_fin_eq (n:ℕ): (Fin n).has_card n := (has_card_iff _ _).mp ⟨ id, Function.bijective_id ⟩theorem SetTheory.Set.Fin_card (n:ℕ): (Fin n).card = n := has_card_to_card (card_fin_eq n)theorem SetTheory.Set.Fin_finite (n:ℕ): (Fin n).finite := ⟨n, card_fin_eq n⟩

theorem SetTheory.Set.EquivCard_to_has_card_eq {X Y:Set} {n: ℕ} (h: X ≈ Y): X.has_card n ↔ Y.has_card n := byinst✝:SetTheoryX:SetY:Setn:ℕh:X ≈ Y⊢ X.has_card n ↔ Y.has_card n
  choose f hf using hinst✝:SetTheoryX:SetY:Setn:ℕf:X.toSubtype → Y.toSubtypehf:Function.Bijective f⊢ X.has_card n ↔ Y.has_card n; let e := Equiv.ofBijective f hfinst✝:SetTheoryX:SetY:Setn:ℕf:X.toSubtype → Y.toSubtypehf:Function.Bijective fe:?_mvar.421075 := Equiv.ofBijective _fvar.421066 _fvar.421071⊢ X.has_card n ↔ Y.has_card n
  constructormpinst✝:SetTheoryX:SetY:Setn:ℕf:X.toSubtype → Y.toSubtypehf:Function.Bijective fe:?_mvar.421075 := Equiv.ofBijective _fvar.421066 _fvar.421071⊢ X.has_card n → Y.has_card nmprinst✝:SetTheoryX:SetY:Setn:ℕf:X.toSubtype → Y.toSubtypehf:Function.Bijective fe:?_mvar.421075 := Equiv.ofBijective _fvar.421066 _fvar.421071⊢ Y.has_card n → X.has_card n <;>mpinst✝:SetTheoryX:SetY:Setn:ℕf:X.toSubtype → Y.toSubtypehf:Function.Bijective fe:?_mvar.421075 := Equiv.ofBijective _fvar.421066 _fvar.421071⊢ X.has_card n → Y.has_card nmprinst✝:SetTheoryX:SetY:Setn:ℕf:X.toSubtype → Y.toSubtypehf:Function.Bijective fe:?_mvar.421075 := Equiv.ofBijective _fvar.421066 _fvar.421071⊢ Y.has_card n → X.has_card n (intro h'mprinst✝:SetTheoryX:SetY:Setn:ℕf:X.toSubtype → Y.toSubtypehf:Function.Bijective fe:?_mvar.421075 := Equiv.ofBijective _fvar.421066 _fvar.421071h':Y.has_card n⊢ X.has_card n; rw [has_card_iff] at *mprinst✝:SetTheoryX:SetY:Setn:ℕf:X.toSubtype → Y.toSubtypehf:Function.Bijective fe:?_mvar.421075 := Equiv.ofBijective _fvar.421066 _fvar.421071h':∃ f, Function.Bijective f⊢ ∃ f, Function.Bijective f; choose g hg using h'mprinst✝:SetTheoryX:SetY:Setn:ℕf:X.toSubtype → Y.toSubtypehf:Function.Bijective fe:?_mvar.421075 := Equiv.ofBijective _fvar.421066 _fvar.421071g:Y.toSubtype → (Fin n).toSubtypehg:Function.Bijective g⊢ ∃ f, Function.Bijective f)
  .mpinst✝:SetTheoryX:SetY:Setn:ℕf:X.toSubtype → Y.toSubtypehf:Function.Bijective fe:?_mvar.421075 := Equiv.ofBijective _fvar.421066 _fvar.421071g:X.toSubtype → (Fin n).toSubtypehg:Function.Bijective g⊢ ∃ f, Function.Bijective f use e.symm.trans (.ofBijective _ hg)hinst✝:SetTheoryX:SetY:Setn:ℕf:X.toSubtype → Y.toSubtypehf:Function.Bijective fe:?_mvar.421075 := Equiv.ofBijective _fvar.421066 _fvar.421071g:X.toSubtype → (Fin n).toSubtypehg:Function.Bijective g⊢ Function.Bijective ⇑(e.symm.trans (Equiv.ofBijective g hg)); apply Equiv.bijectiveAll goals completed! 🐙
  .mprinst✝:SetTheoryX:SetY:Setn:ℕf:X.toSubtype → Y.toSubtypehf:Function.Bijective fe:?_mvar.421075 := Equiv.ofBijective _fvar.421066 _fvar.421071g:Y.toSubtype → (Fin n).toSubtypehg:Function.Bijective g⊢ ∃ f, Function.Bijective f use e.trans (.ofBijective _ hg)hinst✝:SetTheoryX:SetY:Setn:ℕf:X.toSubtype → Y.toSubtypehf:Function.Bijective fe:?_mvar.421075 := Equiv.ofBijective _fvar.421066 _fvar.421071g:Y.toSubtype → (Fin n).toSubtypehg:Function.Bijective g⊢ Function.Bijective ⇑(e.trans (Equiv.ofBijective g hg)); apply Equiv.bijectiveAll goals completed! 🐙

theorem SetTheory.Set.EquivCard_to_card_eq {X Y:Set} (h: X ≈ Y): X.card = Y.card := byinst✝:SetTheoryX:SetY:Seth:X ≈ Y⊢ X.card = Y.card
  by_cases hX: X.finitepos._@._hyg.4279inst✝:SetTheoryX:SetY:Seth:X ≈ YhX:X.finite⊢ X.card = Y.cardneg._@._hyg.4279inst✝:SetTheoryX:SetY:Seth:X ≈ YhX:¬X.finite⊢ X.card = Y.card <;>pos._@._hyg.4279inst✝:SetTheoryX:SetY:Seth:X ≈ YhX:X.finite⊢ X.card = Y.cardneg._@._hyg.4279inst✝:SetTheoryX:SetY:Seth:X ≈ YhX:¬X.finite⊢ X.card = Y.card by_cases hY: Y.finitepos._@._hyg.4334inst✝:SetTheoryX:SetY:Seth:X ≈ YhX:¬X.finitehY:Y.finite⊢ X.card = Y.cardneg._@._hyg.4334inst✝:SetTheoryX:SetY:Seth:X ≈ YhX:¬X.finitehY:¬Y.finite⊢ X.card = Y.card <;>pos._@._hyg.4308inst✝:SetTheoryX:SetY:Seth:X ≈ YhX:X.finitehY:Y.finite⊢ X.card = Y.cardneg._@._hyg.4308inst✝:SetTheoryX:SetY:Seth:X ≈ YhX:X.finitehY:¬Y.finite⊢ X.card = Y.cardpos._@._hyg.4334inst✝:SetTheoryX:SetY:Seth:X ≈ YhX:¬X.finitehY:Y.finite⊢ X.card = Y.cardneg._@._hyg.4334inst✝:SetTheoryX:SetY:Seth:X ≈ YhX:¬X.finitehY:¬Y.finite⊢ X.card = Y.card try rw [finite] at hX hYneg._@._hyg.4334inst✝:SetTheoryX:SetY:Seth:X ≈ YhX:¬∃ n, X.has_card nhY:¬∃ n, Y.has_card n⊢ X.card = Y.card
  .pos._@._hyg.4308inst✝:SetTheoryX:SetY:Seth:X ≈ YhX:∃ n, X.has_card nhY:∃ n, Y.has_card n⊢ X.card = Y.card choose nX hXn using hXpos._@._hyg.4308inst✝:SetTheoryX:SetY:Seth:X ≈ YhY:∃ n, Y.has_card nnX:ℕhXn:X.has_card nX⊢ X.card = Y.card; choose nY hYn using hYpos._@._hyg.4308inst✝:SetTheoryX:SetY:Seth:X ≈ YnX:ℕhXn:X.has_card nXnY:ℕhYn:Y.has_card nY⊢ X.card = Y.card
    simp [has_card_to_card hXn, has_card_to_card hYn, EquivCard_to_has_card_eq h] at *pos._@._hyg.4308inst✝:SetTheoryX:SetY:Seth:X ≈ YnX:ℕnY:ℕhYn:Y.has_card nYhXn:Y.has_card nX⊢ nX = nY
    solve_by_elim [card_uniq]All goals completed! 🐙
  .neg._@._hyg.4308inst✝:SetTheoryX:SetY:Seth:X ≈ YhX:∃ n, X.has_card nhY:¬∃ n, Y.has_card n⊢ X.card = Y.card choose nX hXn using hXneg._@._hyg.4308inst✝:SetTheoryX:SetY:Seth:X ≈ YhY:¬∃ n, Y.has_card nnX:ℕhXn:X.has_card nX⊢ X.card = Y.card; rw [EquivCard_to_has_card_eq h] at hXnneg._@._hyg.4308inst✝:SetTheoryX:SetY:Seth:X ≈ YhY:¬∃ n, Y.has_card nnX:ℕhXn:Y.has_card nX⊢ X.card = Y.card; tautoAll goals completed! 🐙
  .pos._@._hyg.4334inst✝:SetTheoryX:SetY:Seth:X ≈ YhX:¬∃ n, X.has_card nhY:∃ n, Y.has_card n⊢ X.card = Y.card choose nY hYn using hYpos._@._hyg.4334inst✝:SetTheoryX:SetY:Seth:X ≈ YhX:¬∃ n, X.has_card nnY:ℕhYn:Y.has_card nY⊢ X.card = Y.card; rw [←EquivCard_to_has_card_eq h] at hYnpos._@._hyg.4334inst✝:SetTheoryX:SetY:Seth:X ≈ YhX:¬∃ n, X.has_card nnY:ℕhYn:X.has_card nY⊢ X.card = Y.card; tautoAll goals completed! 🐙
  simp [card, hX, hY]All goals completed! 🐙

Вправа 3.6.2

theorem declaration uses 'sorry'SetTheory.Set.empty_iff_card_eq_zero {X:Set} : X = ∅ ↔ X.finite ∧ X.card = 0 := byinst✝:SetTheoryX:Set⊢ X = ∅ ↔ X.finite ∧ X.card = 0
  sorryAll goals completed! 🐙

lemma SetTheory.Set.empty_of_card_eq_zero {X:Set} (hX : X.finite) : X.card = 0 → X = ∅ := byinst✝:SetTheoryX:SethX:X.finite⊢ X.card = 0 → X = ∅
  intro hinst✝:SetTheoryX:SethX:X.finiteh:X.card = 0⊢ X = ∅
  rw [empty_iff_card_eq_zero]inst✝:SetTheoryX:SethX:X.finiteh:X.card = 0⊢ X.finite ∧ X.card = 0
  exact ⟨hX, h⟩All goals completed! 🐙

lemma SetTheory.Set.finite_of_empty {X:Set} : X = ∅ → X.finite := byinst✝:SetTheoryX:Set⊢ X = ∅ → X.finite
  intro hinst✝:SetTheoryX:Seth:X = ∅⊢ X.finite
  rw [empty_iff_card_eq_zero] at hinst✝:SetTheoryX:Seth:X.finite ∧ X.card = 0⊢ X.finite
  exact h.1All goals completed! 🐙

lemma SetTheory.Set.card_eq_zero_of_empty {X:Set} : X = ∅ → X.card = 0 := byinst✝:SetTheoryX:Set⊢ X = ∅ → X.card = 0
  intro hinst✝:SetTheoryX:Seth:X = ∅⊢ X.card = 0
  rw [empty_iff_card_eq_zero] at hinst✝:SetTheoryX:Seth:X.finite ∧ X.card = 0⊢ X.card = 0
  exact h.2All goals completed! 🐙

@[simp]
lemma SetTheory.Set.empty_finite : (∅: Set).finite := finite_of_empty rfl

@[simp]
lemma SetTheory.Set.empty_card_eq_zero : (∅: Set).card = 0 := card_eq_zero_of_empty rfl

Твердження 3.6.14 (a) / Вправа 3.6.4

theorem declaration uses 'sorry'SetTheory.Set.card_insert {X:Set} (hX: X.finite) {x:Object} (hx: x ∉ X) :
    (X ∪ {x}).finite ∧ (X ∪ {x}).card = X.card + 1 := byinst✝:SetTheoryX:SethX:X.finitex:Objecthx:x ∉ X⊢ (X ∪ {x}).finite ∧ (X ∪ {x}).card = X.card + 1 sorryAll goals completed! 🐙

Твердження 3.6.14 (b) / Вправа 3.6.4

theorem declaration uses 'sorry'SetTheory.Set.card_union {X Y:Set} (hX: X.finite) (hY: Y.finite) :
    (X ∪ Y).finite ∧ (X ∪ Y).card ≤ X.card + Y.card := byinst✝:SetTheoryX:SetY:SethX:X.finitehY:Y.finite⊢ (X ∪ Y).finite ∧ (X ∪ Y).card ≤ X.card + Y.card sorryAll goals completed! 🐙

Твердження 3.6.14 (b) / Вправа 3.6.4

theorem declaration uses 'sorry'SetTheory.Set.card_union_disjoint {X Y:Set} (hX: X.finite) (hY: Y.finite)
  (hdisj: Disjoint X Y) : (X ∪ Y).card = X.card + Y.card := byinst✝:SetTheoryX:SetY:SethX:X.finitehY:Y.finitehdisj:Disjoint X Y⊢ (X ∪ Y).card = X.card + Y.card sorryAll goals completed! 🐙

Твердження 3.6.14 (c) / Вправа 3.6.4

theorem declaration uses 'sorry'SetTheory.Set.card_subset {X Y:Set} (hX: X.finite) (hY: Y ⊆ X) :
    Y.finite ∧ Y.card ≤ X.card := byinst✝:SetTheoryX:SetY:SethX:X.finitehY:Y ⊆ X⊢ Y.finite ∧ Y.card ≤ X.card sorryAll goals completed! 🐙

Твердження 3.6.14 (c) / Вправа 3.6.4

theorem declaration uses 'sorry'SetTheory.Set.card_ssubset {X Y:Set} (hX: X.finite) (hY: Y ⊂ X) :
    Y.card < X.card := byinst✝:SetTheoryX:SetY:SethX:X.finitehY:Y ⊂ X⊢ Y.card < X.card sorryAll goals completed! 🐙

Твердження 3.6.14 (d) / Вправа 3.6.4

theorem declaration uses 'sorry'SetTheory.Set.card_image {X Y:Set} (hX: X.finite) (f: X → Y) :
    (image f X).finite ∧ (image f X).card ≤ X.card := byinst✝:SetTheoryX:SetY:SethX:X.finitef:X.toSubtype → Y.toSubtype⊢ (image f X).finite ∧ (image f X).card ≤ X.card sorryAll goals completed! 🐙

Твердження 3.6.14 (d) / Вправа 3.6.4

theorem declaration uses 'sorry'SetTheory.Set.card_image_inj {X Y:Set} (hX: X.finite) {f: X → Y}
  (hf: Function.Injective f) : (image f X).card = X.card := byinst✝:SetTheoryX:SetY:SethX:X.finitef:X.toSubtype → Y.toSubtypehf:Function.Injective f⊢ (image f X).card = X.card sorryAll goals completed! 🐙

Твердження 3.6.14 (e) / Вправа 3.6.4

theorem declaration uses 'sorry'SetTheory.Set.card_prod {X Y:Set} (hX: X.finite) (hY: Y.finite) :
    (X ×ˢ Y).finite ∧ (X ×ˢ Y).card = X.card * Y.card := byinst✝:SetTheoryX:SetY:SethX:X.finitehY:Y.finite⊢ (X ×ˢ Y).finite ∧ (X ×ˢ Y).card = X.card * Y.card sorryAll goals completed! 🐙

noncomputable def declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'SetTheory.Set.pow_fun_equiv {A B : Set} : ↑(A ^ B) ≃ (B → A) where
  toFun := sorry
  invFun := sorry
  left_inv := sorry
  right_inv := sorry

lemma SetTheory.Set.pow_fun_eq_iff {A B : Set} (x y : ↑(A ^ B)) : x = y ↔ pow_fun_equiv x = pow_fun_equiv y := byinst✝:SetTheoryA:SetB:Setx:(A ^ B).toSubtypey:(A ^ B).toSubtype⊢ x = y ↔ pow_fun_equiv x = pow_fun_equiv y
  rw [←pow_fun_equiv.apply_eq_iff_eq]All goals completed! 🐙

Твердження 3.6.14 (f) / Вправа 3.6.4

theorem declaration uses 'sorry'SetTheory.Set.card_pow {X Y:Set} (hY: Y.finite) (hX: X.finite) :
    (Y ^ X).finite ∧ (Y ^ X).card = Y.card ^ X.card := byinst✝:SetTheoryX:SetY:SethY:Y.finitehX:X.finite⊢ (Y ^ X).finite ∧ (Y ^ X).card = Y.card ^ X.card sorryAll goals completed! 🐙

Вправа 3.6.5. You might find Chapter3.SetTheory.Set.prod_commutator.{u_1, u_2} [SetTheory] (X Y : Set) : (X ×ˢ Y).toSubtype ≃ (Y ×ˢ X).toSubtypeSetTheory.Set.prod_commutator useful.

theorem declaration uses 'sorry'SetTheory.Set.prod_EqualCard_prod (A B:Set) :
    EqualCard (A ×ˢ B) (B ×ˢ A) := byinst✝:SetTheoryA:SetB:Set⊢ (A ×ˢ B).EqualCard (B ×ˢ A) sorryAll goals completed! 🐙

noncomputable abbrev SetTheory.Set.pow_fun_equiv' (A B : Set) : ↑(A ^ B) ≃ (B → A) :=
  pow_fun_equiv (A:=A) (B:=B)

Вправа 3.6.6. Вам може знагодитися Chapter3.SetTheory.Set.curry_equiv.{u_1, u_2} [SetTheory] {X Y Z : Set} : (X.toSubtype → Y.toSubtype → Z.toSubtype) ≃ ((X ×ˢ Y).toSubtype → Z.toSubtype)SetTheory.Set.curry_equiv.

theorem declaration uses 'sorry'SetTheory.Set.pow_pow_EqualCard_pow_prod (A B C:Set) :
    EqualCard ((A ^ B) ^ C) (A ^ (B ×ˢ C)) := byinst✝:SetTheoryA:SetB:SetC:Set⊢ ((A ^ B) ^ C).EqualCard (A ^ B ×ˢ C) sorryAll goals completed! 🐙

theorem declaration uses 'sorry'SetTheory.Set.pow_pow_eq_pow_mul (a b c:ℕ): (a^b)^c = a^(b*c) := byinst✝:SetTheorya:ℕb:ℕc:ℕ⊢ (a ^ b) ^ c = a ^ (b * c) sorryAll goals completed! 🐙

theorem declaration uses 'sorry'SetTheory.Set.pow_prod_pow_EqualCard_pow_union (A B C:Set) (hd: Disjoint B C) :
    EqualCard ((A ^ B) ×ˢ (A ^ C)) (A ^ (B ∪ C)) := byinst✝:SetTheoryA:SetB:SetC:Sethd:Disjoint B C⊢ ((A ^ B) ×ˢ (A ^ C)).EqualCard (A ^ (B ∪ C)) sorryAll goals completed! 🐙

theorem declaration uses 'sorry'SetTheory.Set.pow_mul_pow_eq_pow_add (a b c:ℕ): (a^b) * a^c = a^(b+c) := byinst✝:SetTheorya:ℕb:ℕc:ℕ⊢ a ^ b * a ^ c = a ^ (b + c) sorryAll goals completed! 🐙

Вправа 3.6.7

theorem declaration uses 'sorry'SetTheory.Set.injection_iff_card_le {A B:Set} (hA: A.finite) (hB: B.finite) :
    (∃ f:A → B, Function.Injective f) ↔ A.card ≤ B.card := sorry

Вправа 3.6.8

theorem declaration uses 'sorry'SetTheory.Set.surjection_from_injection {A B:Set} (hA: A ≠ ∅) (f: A → B)
  (hf: Function.Injective f) : ∃ g:B → A, Function.Surjective g := byinst✝:SetTheoryA:SetB:SethA:A ≠ ∅f:A.toSubtype → B.toSubtypehf:Function.Injective f⊢ ∃ g, Function.Surjective g sorryAll goals completed! 🐙

Вправа 3.6.9

theorem declaration uses 'sorry'SetTheory.Set.card_union_add_card_inter {A B:Set} (hA: A.finite) (hB: B.finite) :
    A.card + B.card = (A ∪ B).card + (A ∩ B).card := byinst✝:SetTheoryA:SetB:SethA:A.finitehB:B.finite⊢ A.card + B.card = (A ∪ B).card + (A ∩ B).card  sorryAll goals completed! 🐙

Вправа 3.6.10

theorem declaration uses 'sorry'SetTheory.Set.pigeonhole_principle {n:ℕ} {A: Fin n → Set}
  (hA: ∀ i, (A i).finite) (hAcard: (iUnion _ A).card > n) : ∃ i, (A i).card ≥ 2 := byinst✝:SetTheoryn:ℕA:(Fin n).toSubtype → SethA:∀ (i : (Fin n).toSubtype), (A i).finitehAcard:((Fin n).iUnion A).card > n⊢ ∃ i, (A i).card ≥ 2 sorryAll goals completed! 🐙

Вправа 3.6.11

theorem declaration uses 'sorry'SetTheory.Set.two_to_two_iff {X Y:Set} (f: X → Y): Function.Injective f ↔
    ∀ S ⊆ X, S.card = 2 → (image f S).card = 2 := byinst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtype⊢ Function.Injective f ↔ ∀ S ⊆ X, S.card = 2 → (image f S).card = 2 sorryAll goals completed! 🐙

Вправа 3.6.12

def SetTheory.Set.Permutations (n: ℕ): Set := (Fin n ^ Fin n).specify (fun F ↦
    Function.Bijective (pow_fun_equiv F))

Вправа 3.6.12 (i), перша частина

theorem declaration uses 'sorry'SetTheory.Set.Permutations_finite (n: ℕ): (Permutations n).finite := byinst✝:SetTheoryn:ℕ⊢ (Permutations n).finite sorryAll goals completed! 🐙

/- Щоб продовжити Вправу 3.6.12 (i), спершу розв’яжемо деяку теорію про `Permutations` та `Fin`. -/

noncomputable def SetTheory.Set.Permutations_toFun {n: ℕ} (p: Permutations n) : (Fin n) → (Fin n) := byinst✝:SetTheoryn:ℕp:(Permutations n).toSubtype⊢ (Fin n).toSubtype → (Fin n).toSubtype
  have := p.propertyinst✝:SetTheoryn:ℕp:(Permutations n).toSubtypethis:?_mvar.431578 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ (Fin n).toSubtype → (Fin n).toSubtype
  simp only [Permutations, specification_axiom'', powerset_axiom] at thisinst✝:SetTheoryn:ℕp:(Permutations n).toSubtypethis:∃ (h : ∃ f, ↑f = ↑p), Function.Bijective (pow_fun_equiv ⟨↑p, ⋯⟩)⊢ (Fin n).toSubtype → (Fin n).toSubtype
  exact this.choose.chooseAll goals completed! 🐙

theorem declaration uses 'sorry'SetTheory.Set.Permutations_bijective {n: ℕ} (p: Permutations n) :
    Function.Bijective (Permutations_toFun p) := byinst✝:SetTheoryn:ℕp:(Permutations n).toSubtype⊢ Function.Bijective (Permutations_toFun p) sorryAll goals completed! 🐙

theorem declaration uses 'sorry'SetTheory.Set.Permutations_inj {n: ℕ} (p1 p2: Permutations n) :
    Permutations_toFun p1 = Permutations_toFun p2 ↔ p1 = p2 := byinst✝:SetTheoryn:ℕp1:(Permutations n).toSubtypep2:(Permutations n).toSubtype⊢ Permutations_toFun p1 = Permutations_toFun p2 ↔ p1 = p2 sorryAll goals completed! 🐙

Це пов'язує нашу концепцію перестановки з Mathlib-им Equiv.{u_1, u_2} (α : Sort u_1) (β : Sort u_2) : Sort (max (max 1 u_1) u_2)Equiv між Fin sorry : TypeFin Unknown identifier `n`n та Fin sorry : TypeFin Unknown identifier `n`n.

noncomputable def declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'SetTheory.Set.perm_equiv_equiv {n : ℕ} : Permutations n ≃ (Fin n ≃ Fin n) := {
  toFun := fun p => Equiv.ofBijective (Permutations_toFun p) (Permutations_bijective p)
  invFun := sorry
  left_inv := sorry
  right_inv := sorry
}

/- Вправа 3.6.12 включає багато переходів між `Fin n` та `Fin (n + 1}`, тому додамо деякі зручності. -/

Будь-який Fin sorry : TypeFin Unknown identifier `n`n можна перетворити на Fin (sorry + 1) : TypeFin (Unknown identifier `n`n + 1). Порівняйте з Mathlib Fin.castSucc {n : ℕ} : Fin n → Fin (n + 1)Fin.castSucc.

def SetTheory.Set.Fin.castSucc {n} (x : Fin n) : Fin (n + 1) :=
  Fin_embed _ _ (byinst✝:SetTheoryn:ℕx:(Fin n).toSubtype⊢ n ≤ n + 1 omegaAll goals completed! 🐙) x

@[simp]
lemma declaration uses 'sorry'SetTheory.Set.Fin.castSucc_inj {n} {x y : Fin n} : castSucc x = castSucc y ↔ x = y := byinst✝:SetTheoryn:ℕx:(Fin n).toSubtypey:(Fin n).toSubtype⊢ castSucc x = castSucc y ↔ x = y sorryAll goals completed! 🐙

@[simp]
theorem declaration uses 'sorry'SetTheory.Set.Fin.castSucc_ne {n} (x : Fin n) : castSucc x ≠ n := byinst✝:SetTheoryn:ℕx:(Fin n).toSubtype⊢ ↑(castSucc x) ≠ n sorryAll goals completed! 🐙

Будь-який Fin (sorry + 1) : TypeFin (Unknown identifier `n`n + 1), крім Unknown identifier `n`n, можна перетворити на Fin sorry : TypeFin Unknown identifier `n`n. Порівняйте з Mathlib Fin.castPred {n : ℕ} (i : Fin (n + 1)) (h : i ≠ Fin.last n) : Fin nFin.castPred.

noncomputable def SetTheory.Set.Fin.castPred {n} (x : Fin (n + 1)) (h : (x : ℕ) ≠ n) : Fin n :=
  Fin_mk _ (x : ℕ) (byinst✝:SetTheoryn:ℕx:(Fin (n + 1)).toSubtypeh:↑x ≠ n⊢ ↑x < n have := Fin.toNat_lt xinst✝:SetTheoryn:ℕx:(Fin (n + 1)).toSubtypeh:↑x ≠ nthis:?_mvar.438826 := Chapter3.SetTheory.Set.Fin.toNat_lt _fvar.438609⊢ ↑x < n; omegaAll goals completed! 🐙)

@[simp]
theorem declaration uses 'sorry'SetTheory.Set.Fin.castSucc_castPred {n} (x : Fin (n + 1)) (h : (x : ℕ) ≠ n) :
    castSucc (castPred x h) = x := byinst✝:SetTheoryn:ℕx:(Fin (n + 1)).toSubtypeh:↑x ≠ n⊢ castSucc (castPred x h) = x sorryAll goals completed! 🐙

@[simp]
theorem declaration uses 'sorry'SetTheory.Set.Fin.castPred_castSucc {n} (x : Fin n) (h : ((castSucc x : Fin (n + 1)) : ℕ) ≠ n) :
    castPred (castSucc x) h = x := byinst✝:SetTheoryn:ℕx:(Fin n).toSubtypeh:↑(castSucc x) ≠ n⊢ castPred (castSucc x) h = x sorryAll goals completed! 🐙

Будь-яке натуральне число Unknown identifier `n`n можна перетворити на Fin (sorry + 1) : TypeFin (Unknown identifier `n`n + 1). Порівняйте з Mathlib Fin.last (n : ℕ) : Fin (n + 1)Fin.last.

def SetTheory.Set.Fin.last (n : ℕ) : Fin (n + 1) := Fin_mk _ n (byinst✝:SetTheoryn:ℕ⊢ n < n + 1 omegaAll goals completed! 🐙)

Зараз хороший час, щоб довести цей результат, який буде корисним для виконання вправи 3.6.12 (i).

theorem declaration uses 'sorry'SetTheory.Set.card_iUnion_card_disjoint {n m: ℕ} {S : Fin n → Set}
    (hSc : ∀ i, (S i).has_card m)
    (hSd : Pairwise fun i j => Disjoint (S i) (S j)) :
    ((Fin n).iUnion S).finite ∧ ((Fin n).iUnion S).card = n * m := byinst✝:SetTheoryn:ℕm:ℕS:(Fin n).toSubtype → SethSc:∀ (i : (Fin n).toSubtype), (S i).has_card mhSd:Pairwise fun i j => Disjoint (S i) (S j)⊢ ((Fin n).iUnion S).finite ∧ ((Fin n).iUnion S).card = n * m sorryAll goals completed! 🐙

/- Нарешті, ми організуємо спосіб зменшити `Fin (n + 1)` до `Fin n` (або розширити останнє), створюючи "дірку". -/

Якщо деякий ніколи не дорівнює Unknown identifier `i`i, ми можемо зменшити його до Fin sorry : TypeFin Unknown identifier `n`n, зсунувши всі Unknown identifier `x`sorry > sorry : Propx > Unknown identifier `i`i на один вниз. Порівняйте з Mathlib Fin.predAbove {n : ℕ} (p : Fin n) (i : Fin (n + 1)) : Fin nFin.predAbove.

noncomputable def declaration uses 'sorry'declaration uses 'sorry'SetTheory.Set.Fin.predAbove {n} (i : Fin (n + 1)) (x : Fin (n + 1)) (h : x ≠ i) : Fin n :=
  if hx : (x:ℕ) < i then
    Fin_mk _ (x:ℕ) (byinst✝:SetTheoryn:ℕi:(Fin (n + 1)).toSubtypex:(Fin (n + 1)).toSubtypeh:x ≠ ihx:↑x < ↑i⊢ ↑x < n sorryAll goals completed! 🐙)
  else
    Fin_mk _ ((x:ℕ) - 1) (byinst✝:SetTheoryn:ℕi:(Fin (n + 1)).toSubtypex:(Fin (n + 1)).toSubtypeh:x ≠ ihx:¬↑x < ↑i⊢ ↑x - 1 < n sorryAll goals completed! 🐙)

Ми можемо розширити до , зсуваючи всі Unknown identifier `x`sorry ≥ sorry : Propx ≥ Unknown identifier `i`i на один вверх. Результат ніколи не дорівнює Unknown identifier `i`i, тому він утворює обернений процес до зменшення, виконаного Unknown identifier `predAbove`predAbove. Порівняйте з Mathlib Fin.succAbove {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : Fin (n + 1)Fin.succAbove.

noncomputable def declaration uses 'sorry'SetTheory.Set.Fin.succAbove {n} (i : Fin (n + 1)) (x : Fin n) : Fin (n + 1) :=
  if (x:ℕ) < i then
    Fin_embed _ _ (byinst✝:SetTheoryn:ℕi:(Fin (n + 1)).toSubtypex:(Fin n).toSubtype⊢ n ≤ n + 1 sorryAll goals completed! 🐙) x
  else
    Fin_mk _ ((x:ℕ) + 1) (byinst✝:SetTheoryn:ℕi:(Fin (n + 1)).toSubtypex:(Fin n).toSubtype⊢ ↑x + 1 < n + 1 sorryAll goals completed! 🐙)

@[simp]
theorem declaration uses 'sorry'SetTheory.Set.Fin.succAbove_ne {n} (i : Fin (n + 1)) (x : Fin n) : succAbove i x ≠ i := byinst✝:SetTheoryn:ℕi:(Fin (n + 1)).toSubtypex:(Fin n).toSubtype⊢ succAbove i x ≠ i sorryAll goals completed! 🐙

@[simp]
theorem declaration uses 'sorry'SetTheory.Set.Fin.succAbove_predAbove {n} (i : Fin (n + 1)) (x : Fin (n + 1)) (h : x ≠ i) :
    (succAbove i) (predAbove i x h) = x := byinst✝:SetTheoryn:ℕi:(Fin (n + 1)).toSubtypex:(Fin (n + 1)).toSubtypeh:x ≠ i⊢ succAbove i (predAbove i x h) = x sorryAll goals completed! 🐙

@[simp]
theorem declaration uses 'sorry'SetTheory.Set.Fin.predAbove_succAbove {n} (i : Fin (n + 1)) (x : Fin n) :
    (predAbove i) (succAbove i x) (succAbove_ne i x) = x := byinst✝:SetTheoryn:ℕi:(Fin (n + 1)).toSubtypex:(Fin n).toSubtype⊢ predAbove i (succAbove i x) ⋯ = x sorryAll goals completed! 🐙

Вправа 3.6.12 (i), друга частина

theorem declaration uses 'sorry'SetTheory.Set.Permutations_ih (n: ℕ):
    (Permutations (n + 1)).card = (n + 1) * (Permutations n).card := byinst✝:SetTheoryn:ℕ⊢ (Permutations (n + 1)).card = (n + 1) * (Permutations n).card
  let S i := (Permutations (n + 1)).specify (fun p ↦ perm_equiv_equiv p (Fin.last n) = i)inst✝:SetTheoryn:ℕS:(@Chapter3.SetTheory.Set.Fin _fvar.443015 (_fvar.443242 + 1)).toSubtype → Chapter3.Set := 
  fun i =>
    @Chapter3.SetTheory.Set.specify _fvar.443015 (@Chapter3.SetTheory.Set.Permutations _fvar.443015 (_fvar.443242 + 1))
      fun p => (Chapter3.SetTheory.Set.perm_equiv_equiv p) (Chapter3.SetTheory.Set.Fin.last _fvar.443242) = i⊢ (Permutations (n + 1)).card = (n + 1) * (Permutations n).card

  have hSe : ∀ i, S i ≈ Permutations n := byinst✝:SetTheoryn:ℕ⊢ (Permutations (n + 1)).card = (n + 1) * (Permutations n).card
    intro iinst✝:SetTheoryn:ℕS:(@Chapter3.SetTheory.Set.Fin _fvar.443015 (_fvar.443242 + 1)).toSubtype → Chapter3.Set := 
  fun i =>
    @Chapter3.SetTheory.Set.specify _fvar.443015 (@Chapter3.SetTheory.Set.Permutations _fvar.443015 (_fvar.443242 + 1))
      fun p => (Chapter3.SetTheory.Set.perm_equiv_equiv p) (Chapter3.SetTheory.Set.Fin.last _fvar.443242) = ii:(Fin (n + 1)).toSubtype⊢ S i ≈ Permutations n
    -- Підказка: вам можуть стати в нагоді `perm_equiv_equiv`, `Fin.succAbove` та `Fin.predAbove`.
    have equiv : S i ≃ Permutations n := sorryinst✝:SetTheoryn:ℕS:(@Chapter3.SetTheory.Set.Fin _fvar.443015 (_fvar.443242 + 1)).toSubtype → Chapter3.Set := 
  fun i =>
    @Chapter3.SetTheory.Set.specify _fvar.443015 (@Chapter3.SetTheory.Set.Permutations _fvar.443015 (_fvar.443242 + 1))
      fun p => (Chapter3.SetTheory.Set.perm_equiv_equiv p) (Chapter3.SetTheory.Set.Fin.last _fvar.443242) = ii:(Fin (n + 1)).toSubtypeequiv:Chapter3.SetTheory.Set.toSubtype (@_fvar.443511 _fvar.443566) ≃
  (@Chapter3.SetTheory.Set.Permutations _fvar.443015 _fvar.443242).toSubtype := 
  sorry⊢ S i ≈ Permutations n
    use equiv, equiv.injective, equiv.surjectiveAll goals completed! 🐙

  -- Підказка: вам можуть стати в нагоді `card_iUnion_card_disjoint` та `Permutations_finite`.
  sorryAll goals completed! 🐙

Вправа 3.6.12 (ii)

theorem declaration uses 'sorry'SetTheory.Set.Permutations_card (n: ℕ):
    (Permutations n).card = n.factorial := byinst✝:SetTheoryn:ℕ⊢ (Permutations n).card = n.factorial sorryAll goals completed! 🐙

Зв'язки іх Mathlib-ім Finite.{u_3} (α : Sort u_3) : PropFinite

theorem SetTheory.Set.finite_iff_finite {X:Set} : X.finite ↔ Finite X := byinst✝:SetTheoryX:Set⊢ X.finite ↔ Finite X.toSubtype
  rw [finite_iff_exists_equiv_fin, finite]inst✝:SetTheoryX:Set⊢ (∃ n, X.has_card n) ↔ ∃ n, Nonempty (X.toSubtype ≃ _root_.Fin n)
  constructormpinst✝:SetTheoryX:Set⊢ (∃ n, X.has_card n) → ∃ n, Nonempty (X.toSubtype ≃ _root_.Fin n)mprinst✝:SetTheoryX:Set⊢ (∃ n, Nonempty (X.toSubtype ≃ _root_.Fin n)) → ∃ n, X.has_card n
  ·mpinst✝:SetTheoryX:Set⊢ (∃ n, X.has_card n) → ∃ n, Nonempty (X.toSubtype ≃ _root_.Fin n) rintro ⟨n, hn⟩mp.introinst✝:SetTheoryX:Setn:ℕhn:X.has_card n⊢ ∃ n, Nonempty (X.toSubtype ≃ _root_.Fin n)
    use nhinst✝:SetTheoryX:Setn:ℕhn:X.has_card n⊢ Nonempty (X.toSubtype ≃ _root_.Fin n)
    obtain ⟨f, hf⟩ := hnh.introinst✝:SetTheoryX:Setn:ℕf:X.toSubtype → (Fin n).toSubtypehf:Function.Bijective f⊢ Nonempty (X.toSubtype ≃ _root_.Fin n)
    have eq := (Equiv.ofBijective f hf).trans (Fin.Fin_equiv_Fin n)h.introinst✝:SetTheoryX:Setn:ℕf:X.toSubtype → (Fin n).toSubtypehf:Function.Bijective feq:?_mvar.444529 := (Equiv.ofBijective _fvar.444523 _fvar.444524).trans (Chapter3.SetTheory.Set.Fin.Fin_equiv_Fin _fvar.444468)⊢ Nonempty (X.toSubtype ≃ _root_.Fin n)
    exact ⟨eq⟩All goals completed! 🐙
  rintro ⟨n, hn⟩mpr.introinst✝:SetTheoryX:Setn:ℕhn:Nonempty (X.toSubtype ≃ _root_.Fin n)⊢ ∃ n, X.has_card n
  use nhinst✝:SetTheoryX:Setn:ℕhn:Nonempty (X.toSubtype ≃ _root_.Fin n)⊢ X.has_card n
  have eq := hn.some.trans (Fin.Fin_equiv_Fin n).symmhinst✝:SetTheoryX:Setn:ℕhn:Nonempty (X.toSubtype ≃ _root_.Fin n)eq:?_mvar.444627 := Equiv.trans (Nonempty.some _fvar.444590) (Chapter3.SetTheory.Set.Fin.Fin_equiv_Fin _fvar.444589).symm⊢ X.has_card n
  exact ⟨eq, eq.bijective⟩All goals completed! 🐙

Зв'язки іх Mathlib-ім Set.Finite.{u} {α : Type u} (s : _root_.Set α) : PropSet.Finite

theorem SetTheory.Set.finite_iff_set_finite {X:Set} :
    X.finite ↔ (X :_root_.Set Object).Finite := byinst✝:SetTheoryX:Set⊢ X.finite ↔ {x | x ∈ X}.Finite
  rw [finite_iff_finite]inst✝:SetTheoryX:Set⊢ Finite X.toSubtype ↔ {x | x ∈ X}.Finite
  rflAll goals completed! 🐙

Зв'язки із Mathlib-овським Nat.card.{u_3} (α : Type u_3) : ℕNat.card

theorem SetTheory.Set.card_eq_nat_card {X:Set} : X.card = Nat.card X := byinst✝:SetTheoryX:Set⊢ X.card = Nat.card X.toSubtype
  by_cases hf : X.finitepos._@._hyg.7309inst✝:SetTheoryX:Sethf:X.finite⊢ X.card = Nat.card X.toSubtypeneg._@._hyg.7309inst✝:SetTheoryX:Sethf:¬X.finite⊢ X.card = Nat.card X.toSubtype
  ·pos._@._hyg.7309inst✝:SetTheoryX:Sethf:X.finite⊢ X.card = Nat.card X.toSubtype by_cases hz : X.card = 0pos._@._hyg.7336inst✝:SetTheoryX:Sethf:X.finitehz:X.card = 0⊢ X.card = Nat.card X.toSubtypeneg._@._hyg.7336inst✝:SetTheoryX:Sethf:X.finitehz:¬X.card = 0⊢ X.card = Nat.card X.toSubtype
    ·pos._@._hyg.7336inst✝:SetTheoryX:Sethf:X.finitehz:X.card = 0⊢ X.card = Nat.card X.toSubtype rw [hz]pos._@._hyg.7336inst✝:SetTheoryX:Sethf:X.finitehz:X.card = 0⊢ 0 = Nat.card X.toSubtype; symmpos._@._hyg.7336inst✝:SetTheoryX:Sethf:X.finitehz:X.card = 0⊢ Nat.card X.toSubtype = 0
      have : X = ∅ := empty_of_card_eq_zero hf hzpos._@._hyg.7336inst✝:SetTheoryX:Sethf:X.finitehz:X.card = 0this:_fvar.445131 = ∅ := Chapter3.SetTheory.Set.empty_of_card_eq_zero _fvar.445470 _fvar.445550⊢ Nat.card X.toSubtype = 0
      rw [this, Nat.card_eq_zero, isEmpty_iff]pos._@._hyg.7336inst✝:SetTheoryX:Sethf:X.finitehz:X.card = 0this:_fvar.445131 = ∅ := Chapter3.SetTheory.Set.empty_of_card_eq_zero _fvar.445470 _fvar.445550⊢ (∀ (a : ∅.toSubtype), False) ∨ Infinite ∅.toSubtype
      aesopAll goals completed! 🐙
    symmneg._@._hyg.7336inst✝:SetTheoryX:Sethf:X.finitehz:¬X.card = 0⊢ Nat.card X.toSubtype = X.card
    have hc := has_card_card hfneg._@._hyg.7336inst✝:SetTheoryX:Sethf:X.finitehz:¬X.card = 0hc:?_mvar.454775 := Chapter3.SetTheory.Set.has_card_card _fvar.445470⊢ Nat.card X.toSubtype = X.card
    obtain ⟨f, hf⟩ := hcneg.intro._@._hyg.7336inst✝:SetTheoryX:Sethf✝:X.finitehz:¬X.card = 0f:X.toSubtype → (Fin X.card).toSubtypehf:Function.Bijective f⊢ Nat.card X.toSubtype = X.card
    apply Nat.card_eq_of_equiv_finneg.intro.f._@._hyg.7336inst✝:SetTheoryX:Sethf✝:X.finitehz:¬X.card = 0f:X.toSubtype → (Fin X.card).toSubtypehf:Function.Bijective f⊢ X.toSubtype ≃ _root_.Fin X.card
    exact (Equiv.ofBijective f hf).trans (Fin.Fin_equiv_Fin X.card)All goals completed! 🐙
  simp only [card, hf, ↓reduceDIte]neg._@._hyg.7309inst✝:SetTheoryX:Sethf:¬X.finite⊢ 0 = Nat.card X.toSubtype; symmneg._@._hyg.7309inst✝:SetTheoryX:Sethf:¬X.finite⊢ Nat.card X.toSubtype = 0
  rw [Nat.card_eq_zero, ←not_finite_iff_infinite]neg._@._hyg.7309inst✝:SetTheoryX:Sethf:¬X.finite⊢ IsEmpty X.toSubtype ∨ ¬Finite X.toSubtype
  rightneg.h._@._hyg.7309inst✝:SetTheoryX:Sethf:¬X.finite⊢ ¬Finite X.toSubtype
  rwa [finite_iff_set_finite]neg.h._@._hyg.7309inst✝:SetTheoryX:Sethf:¬{x | x ∈ X}.Finite⊢ ¬Finite X.toSubtype at hf

Зв'язки із Mathlib-овським Set.ncard.{u_1} {α : Type u_1} (s : _root_.Set α) : ℕSet.ncard

theorem SetTheory.Set.card_eq_ncard {X:Set} : X.card = (X: _root_.Set Object).ncard := byinst✝:SetTheoryX:Set⊢ X.card = {x | x ∈ X}.ncard
  rw [card_eq_nat_card]inst✝:SetTheoryX:Set⊢ Nat.card X.toSubtype = {x | x ∈ X}.ncard
  rflAll goals completed! 🐙

end Chapter3