Аналіз I, Глава 3.5

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

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

Впорядковані пари та кортежі
Декартові добутки та n-кратні добутки
Зліченний вибіру
Зв'язок із Mathlib аналогами такими як Set.pi.{u_1, u_2} {ι : Type u_1} {α : ι → Type u_2} (s : Set ι) (t : (i : ι) → Set (α i)) : Set ((i : ι) → α i)Set.pi та Set.prod.{u, v} {α : Type u} {β : Type v} (s : Set α) (t : Set β) : Set (α × β)Set.prod

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

Визначення 3.5.1 (Впорядкована пара)

@[ext]
structure OrderedPair where
  fst: Object
  snd: Object

Chapter3.OrderedPair.ext {inst✝ : SetTheory} {x y : OrderedPair} (fst : x.fst = y.fst) (snd : x.snd = y.snd) : x = y#check OrderedPair.ext

Chapter3.OrderedPair.ext {inst✝ : SetTheory} {x y : OrderedPair} (fst : x.fst = y.fst) (snd : x.snd = y.snd) : x = y

Визначення 3.5.1 (Впорядкована пара)

theorem OrderedPair.eq (x y x' y' : Object) :
    (⟨ x, y ⟩ : OrderedPair) = (⟨ x', y' ⟩ : OrderedPair) ↔ x = x' ∧ y = y' := byinst✝:SetTheoryx:Objecty:Objectx':Objecty':Object⊢ { fst := x, snd := y } = { fst := x', snd := y' } ↔ x = x' ∧ y = y' aesopAll goals completed! 🐙

Вправа 3.5.1

abbrev declaration uses 'sorry'OrderedPair.toObject : OrderedPair ↪ Object where
  toFun p := ({ (({p.fst}:Set):Object), (({p.fst, p.snd}:Set):Object) }:Set)
  inj' := byinst✝:SetTheory⊢ Function.Injective fun p =>
  SetTheory.set_to_object {SetTheory.set_to_object {p.fst}, SetTheory.set_to_object {p.fst, p.snd}} sorryAll goals completed! 🐙

instance OrderedPair.inst_coeObject : Coe OrderedPair Object where
  coe := OrderedPair.toObject

Технічна операція перетворююча об'єкт unknown identifier 'x'x та множину unknown identifier 'Y'Y на множину overloaded, errors 1:1 unknown identifier 'x' invalid {...} notation, expected type is not of the form (C ...) Type ?u.63732sorry × sorry : Type (max u_1 u_2){x} × unknown identifier 'Y'Y, необхідна для визначення повного декартового добутку

abbrev SetTheory.Set.slice (x:Object) (Y:Set) : Set :=
  Y.replace (P := fun y z ↦ z = (⟨x, y⟩:OrderedPair)) (byinst✝:SetTheoryx:ObjectY:Set⊢ ∀ (x_1 : Y.toSubtype) (y y' : Object),
  (fun y z => z = OrderedPair.toObject { fst := x, snd := ↑y }) x_1 y ∧
      (fun y z => z = OrderedPair.toObject { fst := x, snd := ↑y }) x_1 y' →
    y = y'
    intro y z z' ⟨ hz, hz'⟩inst✝:SetTheoryx:ObjectY:Sety:Y.toSubtypez:Objectz':Objecthz:(fun y z => z = OrderedPair.toObject { fst := x, snd := ↑y }) y zhz':(fun y z => z = OrderedPair.toObject { fst := x, snd := ↑y }) y z'⊢ z = z'
    simp at hz hz'inst✝:SetTheoryx:ObjectY:Sety:Y.toSubtypez:Objectz':Objecthz:z = set_to_object {set_to_object {x}, set_to_object {x, ↑y}}hz':z' = set_to_object {set_to_object {x}, set_to_object {x, ↑y}}⊢ z = z'
    rw [hz, hz']All goals completed! 🐙
  )

theorem SetTheory.Set.mem_slice (x z:Object) (Y:Set) :
    z ∈ (SetTheory.Set.slice x Y) ↔ ∃ y:Y, z = (⟨x, y⟩:OrderedPair) := replacement_axiom _ _

Визначення 3.5.2 (Декартовий добуток)

abbrev SetTheory.Set.cartesian (X Y:Set) : Set :=
  union (X.replace (P := fun x z ↦ z = slice x Y) (byinst✝:SetTheoryX:SetY:Set⊢ ∀ (x : X.toSubtype) (y y' : Object),
  (fun x z => z = set_to_object (slice (↑x) Y)) x y ∧ (fun x z => z = set_to_object (slice (↑x) Y)) x y' → y = y'
    intro x z z' ⟨ hz, hz' ⟩inst✝:SetTheoryX:SetY:Setx:X.toSubtypez:Objectz':Objecthz:(fun x z => z = set_to_object (slice (↑x) Y)) x zhz':(fun x z => z = set_to_object (slice (↑x) Y)) x z'⊢ z = z'
    simp at hz hz'inst✝:SetTheoryX:SetY:Setx:X.toSubtypez:Objectz':Objecthz:z = set_to_object (slice (↑x) Y)hz':z' = set_to_object (slice (↑x) Y)⊢ z = z'
    rw [hz, hz']All goals completed! 🐙
  ))

Цей екземпляр дозволяє використовувати позначення ×ˢ для декартового добутку.

instance SetTheory.Set.inst_SProd : SProd Set Set Set where
  sprod := cartesian

theorem SetTheory.Set.mem_cartesian (z:Object) (X Y:Set) :
    z ∈ X ×ˢ Y ↔ ∃ x:X, ∃ y:Y, z = (⟨x, y⟩:OrderedPair) := byinst✝:SetTheoryz:ObjectX:SetY:Set⊢ z ∈ X ×ˢ Y ↔ ∃ x y, z = OrderedPair.toObject { fst := ↑x, snd := ↑y }
  simp only [SProd.sprod, union_axiom]inst✝:SetTheoryz:ObjectX:SetY:Set⊢ (∃ S, z ∈ S ∧ set_to_object S ∈ X.replace ⋯) ↔ ∃ x y, z = OrderedPair.toObject { fst := ↑x, snd := ↑y }
  constructormpinst✝:SetTheoryz:ObjectX:SetY:Set⊢ (∃ S, z ∈ S ∧ set_to_object S ∈ X.replace ⋯) → ∃ x y, z = OrderedPair.toObject { fst := ↑x, snd := ↑y }mprinst✝:SetTheoryz:ObjectX:SetY:Set⊢ (∃ x y, z = OrderedPair.toObject { fst := ↑x, snd := ↑y }) → ∃ S, z ∈ S ∧ set_to_object S ∈ X.replace ⋯
  .mpinst✝:SetTheoryz:ObjectX:SetY:Set⊢ (∃ S, z ∈ S ∧ set_to_object S ∈ X.replace ⋯) → ∃ x y, z = OrderedPair.toObject { fst := ↑x, snd := ↑y } intro hmpinst✝:SetTheoryz:ObjectX:SetY:Seth:∃ S, z ∈ S ∧ set_to_object S ∈ X.replace ⋯⊢ ∃ x y, z = OrderedPair.toObject { fst := ↑x, snd := ↑y }
    obtain ⟨ S, hz, hS ⟩ := hmp.intro.introinst✝:SetTheoryz:ObjectX:SetY:SetS:Sethz:z ∈ ShS:set_to_object S ∈ X.replace ⋯⊢ ∃ x y, z = OrderedPair.toObject { fst := ↑x, snd := ↑y }
    rw [replacement_axiom] at hSmp.intro.introinst✝:SetTheoryz:ObjectX:SetY:SetS:Sethz:z ∈ ShS:∃ x, set_to_object S = set_to_object (slice (↑x) Y)⊢ ∃ x y, z = OrderedPair.toObject { fst := ↑x, snd := ↑y }
    obtain ⟨ x, hx ⟩ := hSmp.intro.intro.introinst✝:SetTheoryz:ObjectX:SetY:SetS:Sethz:z ∈ Sx:X.toSubtypehx:set_to_object S = set_to_object (slice (↑x) Y)⊢ ∃ x y, z = OrderedPair.toObject { fst := ↑x, snd := ↑y }
    simp at hxmp.intro.intro.introinst✝:SetTheoryz:ObjectX:SetY:SetS:Sethz:z ∈ Sx:X.toSubtypehx:S = slice (↑x) Y⊢ ∃ x y, z = OrderedPair.toObject { fst := ↑x, snd := ↑y }
    rw [hx] at hzmp.intro.intro.introinst✝:SetTheoryz:ObjectX:SetY:SetS:Setx:X.toSubtypehz:z ∈ slice (↑x) Yhx:S = slice (↑x) Y⊢ ∃ x y, z = OrderedPair.toObject { fst := ↑x, snd := ↑y }
    rw [mem_slice] at hzmp.intro.intro.introinst✝:SetTheoryz:ObjectX:SetY:SetS:Setx:X.toSubtypehz:∃ y, z = OrderedPair.toObject { fst := ↑x, snd := ↑y }hx:S = slice (↑x) Y⊢ ∃ x y, z = OrderedPair.toObject { fst := ↑x, snd := ↑y }
    obtain ⟨ y, rfl ⟩ := hzmp.intro.intro.intro.introinst✝:SetTheoryX:SetY:SetS:Setx:X.toSubtypehx:S = slice (↑x) Yy:Y.toSubtype⊢ ∃ x_1 y_1, OrderedPair.toObject { fst := ↑x, snd := ↑y } = OrderedPair.toObject { fst := ↑x_1, snd := ↑y_1 }
    use x, yAll goals completed! 🐙
  intro hmprinst✝:SetTheoryz:ObjectX:SetY:Seth:∃ x y, z = OrderedPair.toObject { fst := ↑x, snd := ↑y }⊢ ∃ S, z ∈ S ∧ set_to_object S ∈ X.replace ⋯
  obtain ⟨ x, y, rfl ⟩ := hmpr.intro.introinst✝:SetTheoryX:SetY:Setx:X.toSubtypey:Y.toSubtype⊢ ∃ S, OrderedPair.toObject { fst := ↑x, snd := ↑y } ∈ S ∧ set_to_object S ∈ X.replace ⋯
  use slice x Yhinst✝:SetTheoryX:SetY:Setx:X.toSubtypey:Y.toSubtype⊢ OrderedPair.toObject { fst := ↑x, snd := ↑y } ∈ slice (↑x) Y ∧ set_to_object (slice (↑x) Y) ∈ X.replace ⋯
  constructorh.leftinst✝:SetTheoryX:SetY:Setx:X.toSubtypey:Y.toSubtype⊢ OrderedPair.toObject { fst := ↑x, snd := ↑y } ∈ slice (↑x) Yh.rightinst✝:SetTheoryX:SetY:Setx:X.toSubtypey:Y.toSubtype⊢ set_to_object (slice (↑x) Y) ∈ X.replace ⋯
  .h.leftinst✝:SetTheoryX:SetY:Setx:X.toSubtypey:Y.toSubtype⊢ OrderedPair.toObject { fst := ↑x, snd := ↑y } ∈ slice (↑x) Y rw [mem_slice]h.leftinst✝:SetTheoryX:SetY:Setx:X.toSubtypey:Y.toSubtype⊢ ∃ y_1, OrderedPair.toObject { fst := ↑x, snd := ↑y } = OrderedPair.toObject { fst := ↑x, snd := ↑y_1 }
    use yAll goals completed! 🐙
  rw [replacement_axiom]h.rightinst✝:SetTheoryX:SetY:Setx:X.toSubtypey:Y.toSubtype⊢ ∃ x_1, set_to_object (slice (↑x) Y) = set_to_object (slice (↑x_1) Y)
  use xAll goals completed! 🐙

abbrev SetTheory.Set.curry {X Y Z:Set} (f: X ×ˢ Y → Z) : X → Y → Z :=
  fun x y ↦ f ⟨ (⟨ x, y ⟩:OrderedPair), byinst✝:SetTheoryX:SetY:SetZ:Setf:(X ×ˢ Y).toSubtype → Z.toSubtypex:X.toSubtypey:Y.toSubtype⊢ OrderedPair.toObject { fst := ↑x, snd := ↑y } ∈ X ×ˢ Y rw [mem_cartesian]inst✝:SetTheoryX:SetY:SetZ:Setf:(X ×ˢ Y).toSubtype → Z.toSubtypex:X.toSubtypey:Y.toSubtype⊢ ∃ x_1 y_1, OrderedPair.toObject { fst := ↑x, snd := ↑y } = OrderedPair.toObject { fst := ↑x_1, snd := ↑y_1 }; use x, yAll goals completed! 🐙 ⟩

noncomputable abbrev SetTheory.Set.fst {X Y:Set} (z:X ×ˢ Y) : X :=
  (show ∃ x:X, ∃ y:Y, z.val = (⟨ x, y ⟩:OrderedPair)
  byAll goals completed! 🐙 exact (mem_cartesian _ _ _).mp z.propertyAll goals completed! 🐙).choose

noncomputable abbrev SetTheory.Set.snd {X Y:Set} (z:X ×ˢ Y) : Y :=
  (show ∃ y:Y, ∃ x:X, z.val = (⟨ x, y ⟩:OrderedPair)
  byAll goals completed! 🐙 rw [exists_comm]inst✝:SetTheoryX:SetY:Setz:(X ×ˢ Y).toSubtype⊢ ∃ b a, ↑z = OrderedPair.toObject { fst := ↑b, snd := ↑a }; exact (mem_cartesian _ _ _).mp z.propertyAll goals completed! 🐙).choose

theorem SetTheory.Set.pair_eq_fst_snd {X Y:Set} (z:X ×ˢ Y) :
    z.val = (⟨ fst z, snd z ⟩:OrderedPair) := byinst✝:SetTheoryX:SetY:Setz:(X ×ˢ Y).toSubtype⊢ ↑z = OrderedPair.toObject { fst := ↑(fst z), snd := ↑(snd z) }
  obtain ⟨ y, hy ⟩ := ((mem_cartesian _ _ _).mp z.property).choose_specintroinst✝:SetTheoryX:SetY:Setz:(X ×ˢ Y).toSubtypey:Y.toSubtypehy:↑z = OrderedPair.toObject { fst := ↑⋯.choose, snd := ↑y }⊢ ↑z = OrderedPair.toObject { fst := ↑(fst z), snd := ↑(snd z) }
  obtain ⟨ x, hx ⟩ := (exists_comm.mp ((mem_cartesian _ _ _).mp z.property)).choose_specintro.introinst✝:SetTheoryX:SetY:Setz:(X ×ˢ Y).toSubtypey:Y.toSubtypehy:↑z = OrderedPair.toObject { fst := ↑⋯.choose, snd := ↑y }x:X.toSubtypehx:↑z = OrderedPair.toObject { fst := ↑x, snd := ↑⋯.choose }⊢ ↑z = OrderedPair.toObject { fst := ↑(fst z), snd := ↑(snd z) }
  change z.val = (⟨ fst z, y ⟩:OrderedPair) at hyintro.introinst✝:SetTheoryX:SetY:Setz:(X ×ˢ Y).toSubtypey:Y.toSubtypex:X.toSubtypehx:↑z = OrderedPair.toObject { fst := ↑x, snd := ↑⋯.choose }hy:↑z = OrderedPair.toObject { fst := ↑(fst z), snd := ↑y }⊢ ↑z = OrderedPair.toObject { fst := ↑(fst z), snd := ↑(snd z) }
  change z.val = (⟨ x, snd z ⟩:OrderedPair) at hxintro.introinst✝:SetTheoryX:SetY:Setz:(X ×ˢ Y).toSubtypey:Y.toSubtypex:X.toSubtypehy:↑z = OrderedPair.toObject { fst := ↑(fst z), snd := ↑y }hx:↑z = OrderedPair.toObject { fst := ↑x, snd := ↑(snd z) }⊢ ↑z = OrderedPair.toObject { fst := ↑(fst z), snd := ↑(snd z) }
  rw [hx] at hy ⊢intro.introinst✝:SetTheoryX:SetY:Setz:(X ×ˢ Y).toSubtypey:Y.toSubtypex:X.toSubtypehy:OrderedPair.toObject { fst := ↑x, snd := ↑(snd z) } = OrderedPair.toObject { fst := ↑(fst z), snd := ↑y }hx:↑z = OrderedPair.toObject { fst := ↑x, snd := ↑(snd z) }⊢ OrderedPair.toObject { fst := ↑x, snd := ↑(snd z) } = OrderedPair.toObject { fst := ↑(fst z), snd := ↑(snd z) }
  simp only [EmbeddingLike.apply_eq_iff_eq, OrderedPair.eq] at hy ⊢intro.introinst✝:SetTheoryX:SetY:Setz:(X ×ˢ Y).toSubtypey:Y.toSubtypex:X.toSubtypehx:↑z = OrderedPair.toObject { fst := ↑x, snd := ↑(snd z) }hy:↑x = ↑(fst z) ∧ ↑(snd z) = ↑y⊢ ↑x = ↑(fst z) ∧ True
  simp [hy.1]All goals completed! 🐙

noncomputable abbrev SetTheory.Set.uncurry {X Y Z:Set} (f: X → Y → Z) : X ×ˢ Y → Z :=
  fun z ↦ f (fst z) (snd z)

theorem declaration uses 'sorry'SetTheory.Set.curry_uncurry {X Y Z:Set} (f: X → Y → Z) : curry (uncurry f) = f := byinst✝:SetTheoryX:SetY:SetZ:Setf:X.toSubtype → Y.toSubtype → Z.toSubtype⊢ curry (uncurry f) = f sorryAll goals completed! 🐙

theorem declaration uses 'sorry'SetTheory.Set.uncurry_curry {X Y Z:Set} (f: X ×ˢ Y → Z) : uncurry (curry f) = f := byinst✝:SetTheoryX:SetY:SetZ:Setf:(X ×ˢ Y).toSubtype → Z.toSubtype⊢ uncurry (curry f) = f sorryAll goals completed! 🐙

noncomputable abbrev declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'SetTheory.Set.prod_commutator (X Y:Set) : X ×ˢ Y ≃ Y ×ˢ X where
  toFun := sorry
  invFun := sorry
  left_inv := sorry
  right_inv := sorry

noncomputable abbrev declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'SetTheory.Set.prod_associator (X Y Z:Set) : (X ×ˢ Y) ×ˢ Z ≃ X ×ˢ (Y ×ˢ Z) where
  toFun := sorry
  invFun := sorry
  left_inv := sorry
  right_inv := sorry

Прив'язка до Mathlib-овського добутку множин

noncomputable abbrev declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'SetTheory.Set.prod_equiv_prod (X Y:Set) :
    ((X ×ˢ Y):_root_.Set Object) ≃ (X:_root_.Set Object) ×ˢ (Y:_root_.Set Object) where
  toFun := sorry
  invFun := sorry
  left_inv := sorry
  right_inv := sorry

Визначення 3.5.7

abbrev SetTheory.Set.tuple {I:Set} {X: I → Set} (a: ∀ i, X i) : Object :=
  object_of ((fun i ↦ ⟨ a i, byinst✝:SetTheoryI:SetX:I.toSubtype → Seta:(i : I.toSubtype) → (X i).toSubtypei:I.toSubtype⊢ ↑(a i) ∈ I.iUnion X rw [mem_iUnion]inst✝:SetTheoryI:SetX:I.toSubtype → Seta:(i : I.toSubtype) → (X i).toSubtypei:I.toSubtype⊢ ∃ α, ↑(a i) ∈ X α; use ihinst✝:SetTheoryI:SetX:I.toSubtype → Seta:(i : I.toSubtype) → (X i).toSubtypei:I.toSubtype⊢ ↑(a i) ∈ X i; exact (a i).propertyAll goals completed! 🐙 ⟩):I → iUnion I X)

Визначення 3.5.7

abbrev SetTheory.Set.iProd {I: Set} (X: I → Set) : Set :=
  ((iUnion I X)^I).specify (fun t ↦ ∃ a : ∀ i, X i, t = tuple a)

Визначення 3.5.7

theorem SetTheory.Set.mem_iProd {I: Set} {X: I → Set} (t:Object) :
    t ∈ iProd X ↔ ∃ a: ∀ i, X i, t = tuple a := byinst✝:SetTheoryI:SetX:I.toSubtype → Sett:Object⊢ t ∈ iProd X ↔ ∃ a, t = tuple a
  simp only [iProd, specification_axiom'']inst✝:SetTheoryI:SetX:I.toSubtype → Sett:Object⊢ (∃ (_ : t ∈ I.iUnion X ^ I), ∃ a, t = tuple a) ↔ ∃ a, t = tuple a
  constructormpinst✝:SetTheoryI:SetX:I.toSubtype → Sett:Object⊢ (∃ (_ : t ∈ I.iUnion X ^ I), ∃ a, t = tuple a) → ∃ a, t = tuple amprinst✝:SetTheoryI:SetX:I.toSubtype → Sett:Object⊢ (∃ a, t = tuple a) → ∃ (_ : t ∈ I.iUnion X ^ I), ∃ a, t = tuple a
  .mpinst✝:SetTheoryI:SetX:I.toSubtype → Sett:Object⊢ (∃ (_ : t ∈ I.iUnion X ^ I), ∃ a, t = tuple a) → ∃ a, t = tuple a intro ⟨ ht, a, h ⟩mpinst✝:SetTheoryI:SetX:I.toSubtype → Sett:Objectht:t ∈ I.iUnion X ^ Ia:(i : I.toSubtype) → (X i).toSubtypeh:t = tuple a⊢ ∃ a, t = tuple a
    use aAll goals completed! 🐙
  intro ⟨ a, ha ⟩mprinst✝:SetTheoryI:SetX:I.toSubtype → Sett:Objecta:(i : I.toSubtype) → (X i).toSubtypeha:t = tuple a⊢ ∃ (_ : t ∈ I.iUnion X ^ I), ∃ a, t = tuple a
  have h : t ∈ (I.iUnion X)^I := byinst✝:SetTheoryI:SetX:I.toSubtype → Sett:Object⊢ t ∈ iProd X ↔ ∃ a, t = tuple a
    rw [power_set_axiom, ha]inst✝:SetTheoryI:SetX:I.toSubtype → Sett:Objecta:(i : I.toSubtype) → (X i).toSubtypeha:t = tuple a⊢ ∃ f, object_of f = tuple a
    use fun i ↦ ⟨ a i, byinst✝:SetTheoryI:SetX:I.toSubtype → Sett:Objecta:(i : I.toSubtype) → (X i).toSubtypeha:t = tuple ai:I.toSubtype⊢ ↑(a i) ∈ I.iUnion X rw [mem_iUnion]inst✝:SetTheoryI:SetX:I.toSubtype → Sett:Objecta:(i : I.toSubtype) → (X i).toSubtypeha:t = tuple ai:I.toSubtype⊢ ∃ α, ↑(a i) ∈ X α; use ihinst✝:SetTheoryI:SetX:I.toSubtype → Sett:Objecta:(i : I.toSubtype) → (X i).toSubtypeha:t = tuple ai:I.toSubtype⊢ ↑(a i) ∈ X i; exact (a i).propertyAll goals completed! 🐙 ⟩
  use h, aAll goals completed! 🐙

theorem SetTheory.Set.tuple_mem_iProd {I: Set} {X: I → Set} (a: ∀ i, X i) :
    tuple a ∈ iProd X := byinst✝:SetTheoryI:SetX:I.toSubtype → Seta:(i : I.toSubtype) → (X i).toSubtype⊢ tuple a ∈ iProd X rw [mem_iProd]inst✝:SetTheoryI:SetX:I.toSubtype → Seta:(i : I.toSubtype) → (X i).toSubtype⊢ ∃ a_1, tuple a = tuple a_1; use aAll goals completed! 🐙

@[simp]
theorem declaration uses 'sorry'SetTheory.Set.tuple_inj {I:Set} {X: I → Set} (a b: ∀ i, X i) :
    tuple a = tuple b ↔ a = b := byinst✝:SetTheoryI:SetX:I.toSubtype → Seta:(i : I.toSubtype) → (X i).toSubtypeb:(i : I.toSubtype) → (X i).toSubtype⊢ tuple a = tuple b ↔ a = b sorryAll goals completed! 🐙

Приклад 3.5.11. Я підозрюю, що більшість еквівалентностей вимагатимуть класичних міркувань і будуть визначені лише необчислювально, але був би радий дізнатися про контрприклади.

noncomputable abbrev declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'SetTheory.Set.singleton_iProd_equiv (i:Object) (X:Set) :
    iProd (fun _:({i}:Set) ↦ X) ≃ X where
  toFun := sorry
  invFun := sorry
  left_inv := sorry
  right_inv := sorry

Приклад 3.5.11

noncomputable abbrev declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'SetTheory.Set.empty_iProd_equiv (X: (∅:Set) → Set) : iProd X ≃ Unit where
  toFun := sorry
  invFun := sorry
  left_inv := sorry
  right_inv := sorry

Приклад 3.5.11

noncomputable abbrev declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'SetTheory.Set.iProd_of_const_equiv (I:Set) (X: Set) :
    iProd (fun i:I ↦ X) ≃ (I → X) where
  toFun := sorry
  invFun := sorry
  left_inv := sorry
  right_inv := sorry

noncomputable abbrev declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'SetTheory.Set.iProd_equiv_prod (X: ({0,1}:Set) → Set) :
    iProd X ≃ (X ⟨ 0, byinst✝:SetTheoryX:{0, 1}.toSubtype → Set⊢ 0 ∈ {0, 1} simpAll goals completed! 🐙 ⟩) ×ˢ (X ⟨ 1, byinst✝:SetTheoryX:{0, 1}.toSubtype → Set⊢ 1 ∈ {0, 1} simpAll goals completed! 🐙 ⟩) where
  toFun := sorry
  invFun := sorry
  left_inv := sorry
  right_inv := sorry

Приклад 3.5.9

noncomputable abbrev declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'SetTheory.Set.iProd_equiv_prod_triple (X: ({0,1,2}:Set) → Set) :
    iProd X ≃ (X ⟨ 0, byinst✝:SetTheoryX:{0, 1, 2}.toSubtype → Set⊢ 0 ∈ {0, 1, 2} simpAll goals completed! 🐙 ⟩) ×ˢ (X ⟨ 1, byinst✝:SetTheoryX:{0, 1, 2}.toSubtype → Set⊢ 1 ∈ {0, 1, 2} simpAll goals completed! 🐙 ⟩) ×ˢ (X ⟨ 2, byinst✝:SetTheoryX:{0, 1, 2}.toSubtype → Set⊢ 2 ∈ {0, 1, 2} simpAll goals completed! 🐙 ⟩) where
  toFun := sorry
  invFun := sorry
  left_inv := sorry
  right_inv := sorry

Зв'язки із Mathlib-овським Set.pi.{u_1, u_2} {ι : Type u_1} {α : ι → Type u_2} (s : Set ι) (t : (i : ι) → Set (α i)) : Set ((i : ι) → α i)Set.pi

noncomputable abbrev declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'SetTheory.Set.iProd_equiv_pi (I:Set) (X: I → Set) :
    iProd X ≃ Set.pi Set.univ (fun i:I ↦ ((X i):_root_.Set Object)) where
  toFun := sorry
  invFun := sorry
  left_inv := sorry
  right_inv := sorry

/-
Зауваження: між цими еквівалентностями також існують додаткові співвідношення, але це
починає переходити в область теорії категорій вищого порядку, яку ми тут не розглядатимемо.
-/

Тут ми створюємо аналог Mathlib-івських типів Fin sorry : TypeFin unknown identifier 'n'n в рамках теорії множин з Розділу 3, із рудиментарним API.

abbrev SetTheory.Set.Fin (n:ℕ) : Set := nat.specify (fun m ↦ (m:ℕ) < n)

theorem SetTheory.Set.mem_Fin (n:ℕ) (x:Object) : x ∈ Fin n ↔ ∃ m, m < n ∧ x = m := byinst✝:SetTheoryn:ℕx:Object⊢ x ∈ Fin n ↔ ∃ m < n, x = ↑m
  rw [specification_axiom'']inst✝:SetTheoryn:ℕx:Object⊢ (∃ (h : x ∈ nat), nat_equiv.symm ⟨x, h⟩ < n) ↔ ∃ m < n, x = ↑m
  constructormpinst✝:SetTheoryn:ℕx:Object⊢ (∃ (h : x ∈ nat), nat_equiv.symm ⟨x, h⟩ < n) → ∃ m < n, x = ↑mmprinst✝:SetTheoryn:ℕx:Object⊢ (∃ m < n, x = ↑m) → ∃ (h : x ∈ nat), nat_equiv.symm ⟨x, h⟩ < n
  .mpinst✝:SetTheoryn:ℕx:Object⊢ (∃ (h : x ∈ nat), nat_equiv.symm ⟨x, h⟩ < n) → ∃ m < n, x = ↑m intro ⟨ h1, h2 ⟩mpinst✝:SetTheoryn:ℕx:Objecth1:x ∈ nath2:nat_equiv.symm ⟨x, h1⟩ < n⊢ ∃ m < n, x = ↑m
    use ((⟨ x, h1 ⟩:nat):ℕ)hinst✝:SetTheoryn:ℕx:Objecth1:x ∈ nath2:nat_equiv.symm ⟨x, h1⟩ < n⊢ nat_equiv.symm ⟨x, h1⟩ < n ∧ x = ↑(nat_equiv.symm ⟨x, h1⟩)
    simp [h2]hinst✝:SetTheoryn:ℕx:Objecth1:x ∈ nath2:nat_equiv.symm ⟨x, h1⟩ < n⊢ x = ↑(nat_equiv.symm ⟨x, h1⟩)
    calc
      x = (⟨ x, h1 ⟩:nat) := byinst✝:SetTheoryn:ℕx:Objecth1:x ∈ nath2:nat_equiv.symm ⟨x, h1⟩ < n⊢ x = ↑⟨x, h1⟩ rflAll goals completed! 🐙
      _ = _ :=  byinst✝:SetTheoryn:ℕx:Objecth1:x ∈ nath2:nat_equiv.symm ⟨x, h1⟩ < n⊢ ↑⟨x, h1⟩ = ↑(nat_equiv.symm ⟨x, h1⟩) congre_self.e_valinst✝:SetTheoryn:ℕx:Objecth1:x ∈ nath2:nat_equiv.symm ⟨x, h1⟩ < n⊢ x = ↑(nat_equiv.1 (nat_equiv.symm ⟨x, h1⟩)); simpAll goals completed! 🐙
  intro ⟨ m, hm, h ⟩mprinst✝:SetTheoryn:ℕx:Objectm:ℕhm:m < nh:x = ↑m⊢ ∃ (h : x ∈ nat), nat_equiv.symm ⟨x, h⟩ < n
  have hn : x ∈ nat := byinst✝:SetTheoryn:ℕx:Object⊢ x ∈ Fin n ↔ ∃ m < n, x = ↑m rw [h, ←SetTheory.Object.ofnat_eq]inst✝:SetTheoryn:ℕx:Objectm:ℕhm:m < nh:x = ↑m⊢ ↑↑m ∈ nat; exact (m:nat).propertyAll goals completed! 🐙
  use hnhinst✝:SetTheoryn:ℕx:Objectm:ℕhm:m < nh:x = ↑mhn:x ∈ nat⊢ nat_equiv.symm ⟨x, hn⟩ < n
  convert hmh.e'_3inst✝:SetTheoryn:ℕx:Objectm:ℕhm:m < nh:x = ↑mhn:x ∈ nat⊢ nat_equiv.symm ⟨x, hn⟩ = m
  simp [h, Equiv.symm_apply_eq]h.e'_3inst✝:SetTheoryn:ℕx:Objectm:ℕhm:m < nh:x = ↑mhn:x ∈ nat⊢ ⟨↑m, ⋯⟩ = nat_equiv m
  rflAll goals completed! 🐙

abbrev SetTheory.Set.Fin_mk (n m:ℕ) (h: m < n): Fin n := ⟨ m, byinst✝:SetTheoryn:ℕm:ℕh:m < n⊢ ↑m ∈ Fin n rw [mem_Fin]inst✝:SetTheoryn:ℕm:ℕh:m < n⊢ ∃ m_1 < n, ↑m = ↑m_1; use mAll goals completed! 🐙 ⟩

theorem SetTheory.Set.mem_Fin' {n:ℕ} (x:Fin n) : ∃ m, ∃ h : m < n, x = Fin_mk n m h := byinst✝:SetTheoryn:ℕx:(Fin n).toSubtype⊢ ∃ m, ∃ (h : m < n), x = Fin_mk n m h
  have := x.propertyinst✝:SetTheoryn:ℕx:(Fin n).toSubtypethis:↑x ∈ Fin n⊢ ∃ m, ∃ (h : m < n), x = Fin_mk n m h
  rw [mem_Fin] at thisinst✝:SetTheoryn:ℕx:(Fin n).toSubtypethis:∃ m < n, ↑x = ↑m⊢ ∃ m, ∃ (h : m < n), x = Fin_mk n m h
  obtain ⟨ m, hm, this ⟩ := thisintro.introinst✝:SetTheoryn:ℕx:(Fin n).toSubtypem:ℕhm:m < nthis:↑x = ↑m⊢ ∃ m, ∃ (h : m < n), x = Fin_mk n m h
  use m, hmhinst✝:SetTheoryn:ℕx:(Fin n).toSubtypem:ℕhm:m < nthis:↑x = ↑m⊢ x = Fin_mk n m hm
  simp [Fin_mk, ←Subtype.val_inj, this]All goals completed! 🐙

abbrev SetTheory.Set.Fin_embed (n N:ℕ) (h: n ≤ N) (i: Fin n) : Fin N := ⟨ i.val, byinst✝:SetTheoryn:ℕN:ℕh:n ≤ Ni:(Fin n).toSubtype⊢ ↑i ∈ Fin N
  have := i.propertyinst✝:SetTheoryn:ℕN:ℕh:n ≤ Ni:(Fin n).toSubtypethis:↑i ∈ Fin n⊢ ↑i ∈ Fin N
  rw [mem_Fin] at this ⊢inst✝:SetTheoryn:ℕN:ℕh:n ≤ Ni:(Fin n).toSubtypethis:∃ m < n, ↑i = ↑m⊢ ∃ m < N, ↑i = ↑m
  obtain ⟨ m, hm, im ⟩ := thisintro.introinst✝:SetTheoryn:ℕN:ℕh:n ≤ Ni:(Fin n).toSubtypem:ℕhm:m < nim:↑i = ↑m⊢ ∃ m < N, ↑i = ↑m
  use m, byinst✝:SetTheoryn:ℕN:ℕh:n ≤ Ni:(Fin n).toSubtypem:ℕhm:m < nim:↑i = ↑m⊢ m < N linarithAll goals completed! 🐙
⟩

Я підозрюю, що ця еквівалентність необчислювана і вимагає класичної логіки, хіба що існує якийсь хитромудрий трюк.

noncomputable abbrev declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'SetTheory.Set.Fin_equiv_Fin (n:ℕ) : Fin n ≃ _root_.Fin n where
  toFun := sorry
  invFun := sorry
  left_inv := sorry
  right_inv := sorry

Лема 3.5.12 (зліченний вибір)

theorem SetTheory.Set.finite_choice {n:ℕ} {X: Fin n → Set} (h: ∀ i, X i ≠ ∅) : iProd X ≠ ∅ := byinst✝:SetTheoryn:ℕX:(Fin n).toSubtype → Seth:∀ (i : (Fin n).toSubtype), X i ≠ ∅⊢ iProd X ≠ ∅
  -- Цей доказ загалом повторює доказ у тексті
  -- (хоча зручніше проводити індукцію від 0, а не від 1)
  induction' n with n hnzeroinst✝:SetTheoryX:(Fin 0).toSubtype → Seth:∀ (i : (Fin 0).toSubtype), X i ≠ ∅⊢ iProd X ≠ ∅succinst✝:SetTheoryn:ℕhn:∀ {X : (Fin n).toSubtype → Set}, (∀ (i : (Fin n).toSubtype), X i ≠ ∅) → iProd X ≠ ∅X:(Fin (n + 1)).toSubtype → Seth:∀ (i : (Fin (n + 1)).toSubtype), X i ≠ ∅⊢ iProd X ≠ ∅
  .zeroinst✝:SetTheoryX:(Fin 0).toSubtype → Seth:∀ (i : (Fin 0).toSubtype), X i ≠ ∅⊢ iProd X ≠ ∅ have : Fin 0 = ∅ := byinst✝:SetTheoryn:ℕX:(Fin n).toSubtype → Seth:∀ (i : (Fin n).toSubtype), X i ≠ ∅⊢ iProd X ≠ ∅
      rw [eq_empty_iff_forall_notMem]inst✝:SetTheoryX:(Fin 0).toSubtype → Seth:∀ (i : (Fin 0).toSubtype), X i ≠ ∅⊢ ∀ (x : Object), x ∉ Fin 0
      intro xinst✝:SetTheoryX:(Fin 0).toSubtype → Seth:∀ (i : (Fin 0).toSubtype), X i ≠ ∅x:Object⊢ x ∉ Fin 0
      by_contra! hinst✝:SetTheoryX:(Fin 0).toSubtype → Seth✝:∀ (i : (Fin 0).toSubtype), X i ≠ ∅x:Objecth:x ∈ Fin 0⊢ False
      rw [specification_axiom''] at hinst✝:SetTheoryX:(Fin 0).toSubtype → Seth✝:∀ (i : (Fin 0).toSubtype), X i ≠ ∅x:Objecth:∃ (h : x ∈ nat), nat_equiv.symm ⟨x, h⟩ < 0⊢ False
      simp at hAll goals completed! 🐙
    have empty (i:Fin 0) : X i := False.elim (byinst✝:SetTheoryX:(Fin 0).toSubtype → Seth:∀ (i : (Fin 0).toSubtype), X i ≠ ∅this:Fin 0 = ∅i:(Fin 0).toSubtype⊢ False rw [this] at iinst✝:SetTheoryX:(Fin 0).toSubtype → Seth:∀ (i : (Fin 0).toSubtype), X i ≠ ∅this:Fin 0 = ∅i:∅.toSubtype⊢ False; exact not_mem_empty i i.propertyAll goals completed! 🐙)
    apply nonempty_of_inhabited (x := tuple empty)zeroinst✝:SetTheoryX:(Fin 0).toSubtype → Seth:∀ (i : (Fin 0).toSubtype), X i ≠ ∅this:Fin 0 = ∅empty:(i : (Fin 0).toSubtype) → (X i).toSubtype⊢ tuple empty ∈ iProd X
    rw [mem_iProd]zeroinst✝:SetTheoryX:(Fin 0).toSubtype → Seth:∀ (i : (Fin 0).toSubtype), X i ≠ ∅this:Fin 0 = ∅empty:(i : (Fin 0).toSubtype) → (X i).toSubtype⊢ ∃ a, tuple empty = tuple a
    use emptyAll goals completed! 🐙
  set X' : Fin n → Set := fun i ↦ X (Fin_embed n (n+1) (byinst✝:SetTheoryn:ℕhn:∀ {X : (Fin n).toSubtype → Set}, (∀ (i : (Fin n).toSubtype), X i ≠ ∅) → iProd X ≠ ∅X:(Fin (n + 1)).toSubtype → Seth:∀ (i : (Fin (n + 1)).toSubtype), X i ≠ ∅i:(Fin n).toSubtype⊢ n ≤ n + 1 linarithAll goals completed! 🐙) i)
  have hX' (i: Fin n) : X' i ≠ ∅ := h _succinst✝:SetTheoryn:ℕhn:∀ {X : (Fin n).toSubtype → Set}, (∀ (i : (Fin n).toSubtype), X i ≠ ∅) → iProd X ≠ ∅X:(Fin (n + 1)).toSubtype → Seth:∀ (i : (Fin (n + 1)).toSubtype), X i ≠ ∅X':(Fin n).toSubtype → Set := fun i => X (Fin_embed n (n + 1) ⋯ i)hX':∀ (i : (Fin n).toSubtype), X' i ≠ ∅⊢ iProd X ≠ ∅
  specialize hn hX'succinst✝:SetTheoryn:ℕX:(Fin (n + 1)).toSubtype → Seth:∀ (i : (Fin (n + 1)).toSubtype), X i ≠ ∅X':(Fin n).toSubtype → Set := fun i => X (Fin_embed n (n + 1) ⋯ i)hX':∀ (i : (Fin n).toSubtype), X' i ≠ ∅hn:iProd X' ≠ ∅⊢ iProd X ≠ ∅
  obtain ⟨ x'_obj, hx' ⟩ := nonempty_def hnsucc.introinst✝:SetTheoryn:ℕX:(Fin (n + 1)).toSubtype → Seth:∀ (i : (Fin (n + 1)).toSubtype), X i ≠ ∅X':(Fin n).toSubtype → Set := fun i => X (Fin_embed n (n + 1) ⋯ i)hX':∀ (i : (Fin n).toSubtype), X' i ≠ ∅hn:iProd X' ≠ ∅x'_obj:Objecthx':x'_obj ∈ iProd X'⊢ iProd X ≠ ∅
  rw [mem_iProd] at hx'succ.introinst✝:SetTheoryn:ℕX:(Fin (n + 1)).toSubtype → Seth:∀ (i : (Fin (n + 1)).toSubtype), X i ≠ ∅X':(Fin n).toSubtype → Set := fun i => X (Fin_embed n (n + 1) ⋯ i)hX':∀ (i : (Fin n).toSubtype), X' i ≠ ∅hn:iProd X' ≠ ∅x'_obj:Objecthx':∃ a, x'_obj = tuple a⊢ iProd X ≠ ∅
  obtain ⟨ x', rfl ⟩ := hx'succ.intro.introinst✝:SetTheoryn:ℕX:(Fin (n + 1)).toSubtype → Seth:∀ (i : (Fin (n + 1)).toSubtype), X i ≠ ∅X':(Fin n).toSubtype → Set := fun i => X (Fin_embed n (n + 1) ⋯ i)hX':∀ (i : (Fin n).toSubtype), X' i ≠ ∅hn:iProd X' ≠ ∅x':(i : (Fin n).toSubtype) → (X' i).toSubtype⊢ iProd X ≠ ∅
  set last : Fin (n+1) := Fin_mk (n+1) n (byinst✝:SetTheoryn:ℕX:(Fin (n + 1)).toSubtype → Seth:∀ (i : (Fin (n + 1)).toSubtype), X i ≠ ∅X':(Fin n).toSubtype → Set := fun i => X (Fin_embed n (n + 1) ⋯ i)hX':∀ (i : (Fin n).toSubtype), X' i ≠ ∅hn:iProd X' ≠ ∅x':(i : (Fin n).toSubtype) → (X' i).toSubtype⊢ n < n + 1 linarithAll goals completed! 🐙)
  obtain ⟨ a, ha ⟩ := nonempty_def (h last)succ.intro.intro.introinst✝:SetTheoryn:ℕX:(Fin (n + 1)).toSubtype → Seth:∀ (i : (Fin (n + 1)).toSubtype), X i ≠ ∅X':(Fin n).toSubtype → Set := fun i => X (Fin_embed n (n + 1) ⋯ i)hX':∀ (i : (Fin n).toSubtype), X' i ≠ ∅hn:iProd X' ≠ ∅x':(i : (Fin n).toSubtype) → (X' i).toSubtypelast:(Fin (n + 1)).toSubtype := Fin_mk (n + 1) n ⋯a:Objectha:a ∈ X last⊢ iProd X ≠ ∅
  set x : ∀ i, X i := byinst✝:SetTheoryn:ℕX:(Fin (n + 1)).toSubtype → Seth:∀ (i : (Fin (n + 1)).toSubtype), X i ≠ ∅X':(Fin n).toSubtype → Set := fun i => X (Fin_embed n (n + 1) ⋯ i)hX':∀ (i : (Fin n).toSubtype), X' i ≠ ∅hn:iProd X' ≠ ∅x':(i : (Fin n).toSubtype) → (X' i).toSubtypelast:(Fin (n + 1)).toSubtype := Fin_mk (n + 1) n ⋯a:Objectha:a ∈ X last⊢ (i : (Fin (n + 1)).toSubtype) → (X i).toSubtype
    intro iinst✝:SetTheoryn:ℕX:(Fin (n + 1)).toSubtype → Seth:∀ (i : (Fin (n + 1)).toSubtype), X i ≠ ∅X':(Fin n).toSubtype → Set := fun i => X (Fin_embed n (n + 1) ⋯ i)hX':∀ (i : (Fin n).toSubtype), X' i ≠ ∅hn:iProd X' ≠ ∅x':(i : (Fin n).toSubtype) → (X' i).toSubtypelast:(Fin (n + 1)).toSubtype := Fin_mk (n + 1) n ⋯a:Objectha:a ∈ X lasti:(Fin (n + 1)).toSubtype⊢ (X i).toSubtype
    have := mem_Fin' iinst✝:SetTheoryn:ℕX:(Fin (n + 1)).toSubtype → Seth:∀ (i : (Fin (n + 1)).toSubtype), X i ≠ ∅X':(Fin n).toSubtype → Set := fun i => X (Fin_embed n (n + 1) ⋯ i)hX':∀ (i : (Fin n).toSubtype), X' i ≠ ∅hn:iProd X' ≠ ∅x':(i : (Fin n).toSubtype) → (X' i).toSubtypelast:(Fin (n + 1)).toSubtype := Fin_mk (n + 1) n ⋯a:Objectha:a ∈ X lasti:(Fin (n + 1)).toSubtypethis:∃ m, ∃ (h : m < n + 1), i = Fin_mk (n + 1) m h⊢ (X i).toSubtype
    classical
    -- На жаль, для виконання цього склеювання потрібна класична логіка;
    -- це тому, що `nat` технічно не є індуктивним типом. Повинно бути якесь обхідне рішення,
    -- що включає еквівалентність між `nat` та `ℕ` (який є індуктивним типом).
    cases decEq i last with
      | isTrue heq =>isTrueinst✝:SetTheoryn:ℕX:(Fin (n + 1)).toSubtype → Seth:∀ (i : (Fin (n + 1)).toSubtype), X i ≠ ∅X':(Fin n).toSubtype → Set := fun i => X (Fin_embed n (n + 1) ⋯ i)hX':∀ (i : (Fin n).toSubtype), X' i ≠ ∅hn:iProd X' ≠ ∅x':(i : (Fin n).toSubtype) → (X' i).toSubtypelast:(Fin (n + 1)).toSubtype := Fin_mk (n + 1) n ⋯a:Objectha:a ∈ X lasti:(Fin (n + 1)).toSubtypethis:∃ m, ∃ (h : m < n + 1), i = Fin_mk (n + 1) m hheq:i = last⊢ (X i).toSubtype
        rw [heq]isTrueinst✝:SetTheoryn:ℕX:(Fin (n + 1)).toSubtype → Seth:∀ (i : (Fin (n + 1)).toSubtype), X i ≠ ∅X':(Fin n).toSubtype → Set := fun i => X (Fin_embed n (n + 1) ⋯ i)hX':∀ (i : (Fin n).toSubtype), X' i ≠ ∅hn:iProd X' ≠ ∅x':(i : (Fin n).toSubtype) → (X' i).toSubtypelast:(Fin (n + 1)).toSubtype := Fin_mk (n + 1) n ⋯a:Objectha:a ∈ X lasti:(Fin (n + 1)).toSubtypethis:∃ m, ∃ (h : m < n + 1), i = Fin_mk (n + 1) m hheq:i = last⊢ (X last).toSubtype
        exact ⟨ a, ha ⟩All goals completed! 🐙
      | isFalse heq =>isFalseinst✝:SetTheoryn:ℕX:(Fin (n + 1)).toSubtype → Seth:∀ (i : (Fin (n + 1)).toSubtype), X i ≠ ∅X':(Fin n).toSubtype → Set := fun i => X (Fin_embed n (n + 1) ⋯ i)hX':∀ (i : (Fin n).toSubtype), X' i ≠ ∅hn:iProd X' ≠ ∅x':(i : (Fin n).toSubtype) → (X' i).toSubtypelast:(Fin (n + 1)).toSubtype := Fin_mk (n + 1) n ⋯a:Objectha:a ∈ X lasti:(Fin (n + 1)).toSubtypethis:∃ m, ∃ (h : m < n + 1), i = Fin_mk (n + 1) m hheq:¬i = last⊢ (X i).toSubtype
        have : ∃ m, ∃ h: m < n, X i = X' (Fin_mk n m h) := byinst✝:SetTheoryn:ℕX:(Fin (n + 1)).toSubtype → Seth:∀ (i : (Fin (n + 1)).toSubtype), X i ≠ ∅X':(Fin n).toSubtype → Set := fun i => X (Fin_embed n (n + 1) ⋯ i)hX':∀ (i : (Fin n).toSubtype), X' i ≠ ∅hn:iProd X' ≠ ∅x':(i : (Fin n).toSubtype) → (X' i).toSubtypelast:(Fin (n + 1)).toSubtype := Fin_mk (n + 1) n ⋯a:Objectha:a ∈ X last⊢ (i : (Fin (n + 1)).toSubtype) → (X i).toSubtype
          obtain ⟨ m, h, this ⟩ := thisintro.introinst✝:SetTheoryn:ℕX:(Fin (n + 1)).toSubtype → Seth✝:∀ (i : (Fin (n + 1)).toSubtype), X i ≠ ∅X':(Fin n).toSubtype → Set := fun i => X (Fin_embed n (n + 1) ⋯ i)hX':∀ (i : (Fin n).toSubtype), X' i ≠ ∅hn:iProd X' ≠ ∅x':(i : (Fin n).toSubtype) → (X' i).toSubtypelast:(Fin (n + 1)).toSubtype := Fin_mk (n + 1) n ⋯a:Objectha:a ∈ X lasti:(Fin (n + 1)).toSubtypeheq:¬i = lastm:ℕh:m < n + 1this:i = Fin_mk (n + 1) m h⊢ ∃ m, ∃ (h : m < n), X i = X' (Fin_mk n m h)
          have h' : m ≠ n := byinst✝:SetTheoryn:ℕX:(Fin (n + 1)).toSubtype → Seth:∀ (i : (Fin (n + 1)).toSubtype), X i ≠ ∅X':(Fin n).toSubtype → Set := fun i => X (Fin_embed n (n + 1) ⋯ i)hX':∀ (i : (Fin n).toSubtype), X' i ≠ ∅hn:iProd X' ≠ ∅x':(i : (Fin n).toSubtype) → (X' i).toSubtypelast:(Fin (n + 1)).toSubtype := Fin_mk (n + 1) n ⋯a:Objectha:a ∈ X last⊢ (i : (Fin (n + 1)).toSubtype) → (X i).toSubtype
            contrapose! heqinst✝:SetTheoryn:ℕX:(Fin (n + 1)).toSubtype → Seth✝:∀ (i : (Fin (n + 1)).toSubtype), X i ≠ ∅X':(Fin n).toSubtype → Set := fun i => X (Fin_embed n (n + 1) ⋯ i)hX':∀ (i : (Fin n).toSubtype), X' i ≠ ∅hn:iProd X' ≠ ∅x':(i : (Fin n).toSubtype) → (X' i).toSubtypelast:(Fin (n + 1)).toSubtype := Fin_mk (n + 1) n ⋯a:Objectha:a ∈ X lasti:(Fin (n + 1)).toSubtypem:ℕh:m < n + 1this:i = Fin_mk (n + 1) m hheq:m = n⊢ i = last
            simp [this, last, heq]All goals completed! 🐙
          replace h' : m < n := byinst✝:SetTheoryn:ℕX:(Fin (n + 1)).toSubtype → Seth:∀ (i : (Fin (n + 1)).toSubtype), X i ≠ ∅X':(Fin n).toSubtype → Set := fun i => X (Fin_embed n (n + 1) ⋯ i)hX':∀ (i : (Fin n).toSubtype), X' i ≠ ∅hn:iProd X' ≠ ∅x':(i : (Fin n).toSubtype) → (X' i).toSubtypelast:(Fin (n + 1)).toSubtype := Fin_mk (n + 1) n ⋯a:Objectha:a ∈ X last⊢ (i : (Fin (n + 1)).toSubtype) → (X i).toSubtype contrapose! h'inst✝:SetTheoryn:ℕX:(Fin (n + 1)).toSubtype → Seth✝:∀ (i : (Fin (n + 1)).toSubtype), X i ≠ ∅X':(Fin n).toSubtype → Set := fun i => X (Fin_embed n (n + 1) ⋯ i)hX':∀ (i : (Fin n).toSubtype), X' i ≠ ∅hn:iProd X' ≠ ∅x':(i : (Fin n).toSubtype) → (X' i).toSubtypelast:(Fin (n + 1)).toSubtype := Fin_mk (n + 1) n ⋯a:Objectha:a ∈ X lasti:(Fin (n + 1)).toSubtypeheq:¬i = lastm:ℕh:m < n + 1this:i = Fin_mk (n + 1) m hh':n ≤ m⊢ m = n; linarithAll goals completed! 🐙
          use m, h'hinst✝:SetTheoryn:ℕX:(Fin (n + 1)).toSubtype → Seth✝:∀ (i : (Fin (n + 1)).toSubtype), X i ≠ ∅X':(Fin n).toSubtype → Set := fun i => X (Fin_embed n (n + 1) ⋯ i)hX':∀ (i : (Fin n).toSubtype), X' i ≠ ∅hn:iProd X' ≠ ∅x':(i : (Fin n).toSubtype) → (X' i).toSubtypelast:(Fin (n + 1)).toSubtype := Fin_mk (n + 1) n ⋯a:Objectha:a ∈ X lasti:(Fin (n + 1)).toSubtypeheq:¬i = lastm:ℕh:m < n + 1this:i = Fin_mk (n + 1) m hh':m < n⊢ X i = X' (Fin_mk n m h')
          simp [X']hinst✝:SetTheoryn:ℕX:(Fin (n + 1)).toSubtype → Seth✝:∀ (i : (Fin (n + 1)).toSubtype), X i ≠ ∅X':(Fin n).toSubtype → Set := fun i => X (Fin_embed n (n + 1) ⋯ i)hX':∀ (i : (Fin n).toSubtype), X' i ≠ ∅hn:iProd X' ≠ ∅x':(i : (Fin n).toSubtype) → (X' i).toSubtypelast:(Fin (n + 1)).toSubtype := Fin_mk (n + 1) n ⋯a:Objectha:a ∈ X lasti:(Fin (n + 1)).toSubtypeheq:¬i = lastm:ℕh:m < n + 1this:i = Fin_mk (n + 1) m hh':m < n⊢ X i = X (Fin_embed n (n + 1) ⋯ (Fin_mk n m h')); congrAll goals completed! 🐙
        rw [this.choose_spec.choose_spec]isFalseinst✝:SetTheoryn:ℕX:(Fin (n + 1)).toSubtype → Seth:∀ (i : (Fin (n + 1)).toSubtype), X i ≠ ∅X':(Fin n).toSubtype → Set := fun i => X (Fin_embed n (n + 1) ⋯ i)hX':∀ (i : (Fin n).toSubtype), X' i ≠ ∅hn:iProd X' ≠ ∅x':(i : (Fin n).toSubtype) → (X' i).toSubtypelast:(Fin (n + 1)).toSubtype := Fin_mk (n + 1) n ⋯a:Objectha:a ∈ X lasti:(Fin (n + 1)).toSubtypethis✝:∃ m, ∃ (h : m < n + 1), i = Fin_mk (n + 1) m hheq:¬i = lastthis:∃ m, ∃ (h : m < n), X i = X' (Fin_mk n m h)⊢ (X' (Fin_mk n this.choose ⋯)).toSubtype
        exact x' _All goals completed! 🐙
  exact nonempty_of_inhabited (tuple_mem_iProd x)All goals completed! 🐙

Вправа 3.5.1, друга частина (вимагає аксіоми регулярності)

abbrev declaration uses 'sorry'OrderedPair.toObject' : OrderedPair ↪ Object where
  toFun p := ({ p.fst, (({p.fst, p.snd}:Set):Object) }:Set)
  inj' := byinst✝:SetTheory⊢ Function.Injective fun p => SetTheory.set_to_object {p.fst, SetTheory.set_to_object {p.fst, p.snd}} sorryAll goals completed! 🐙

Альтернативне визначення кортежу, використане у Вправі 3.5.2

@[ext]
structure SetTheory.Set.Tuple (n:ℕ) where
  X: Set
  x: SetTheory.Set.Fin n → X
  surj: Function.Surjective x

Вправа 3.5.2

theorem declaration uses 'sorry'SetTheory.Set.Tuple.eq {n:ℕ} (t t':Tuple n) :
    t = t' ↔ ∀ n : Fin n, ((t.x n):Object) = ((t'.x n):Object) := byinst✝:SetTheoryn:ℕt:Tuple nt':Tuple n⊢ t = t' ↔ ∀ (n_1 : (Fin n).toSubtype), ↑(t.x n_1) = ↑(t'.x n_1) sorryAll goals completed! 🐙

noncomputable abbrev declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'SetTheory.Set.iProd_equiv_tuples (n:ℕ) (X: Fin n → Set) :
    iProd X ≃ { t:Tuple n // ∀ i, (t.x i:Object) ∈ X i } where
  toFun := sorry
  invFun := sorry
  left_inv := sorry
  right_inv := sorry

Вправа 3.5.3. Дух завдання полягає в тому, щоб уникнути прямих переписувань (які роблять усі ці твердження тривіальними), а натомість використовувати unknown identifier 'OrderedPair.eq'OrderedPair.eq або unknown identifier 'SetTheory.Set.tuple_inj'SetTheory.Set.tuple_inj

theorem declaration uses 'sorry'OrderedPair.refl (p: OrderedPair) : p = p := byinst✝:SetTheoryp:OrderedPair⊢ p = p sorryAll goals completed! 🐙

theorem declaration uses 'sorry'OrderedPair.symm (p q: OrderedPair) : p = q ↔ q = p := byinst✝:SetTheoryp:OrderedPairq:OrderedPair⊢ p = q ↔ q = p sorryAll goals completed! 🐙

theorem declaration uses 'sorry'OrderedPair.trans {p q r: OrderedPair} (hpq: p=q) (hqr: q=r) : p=r := byinst✝:SetTheoryp:OrderedPairq:OrderedPairr:OrderedPairhpq:p = qhqr:q = r⊢ p = r sorryAll goals completed! 🐙

theorem declaration uses 'sorry'SetTheory.Set.tuple_refl {I:Set} {X: I → Set} (a: ∀ i, X i) :
    tuple a = tuple a := byinst✝:SetTheoryI:SetX:I.toSubtype → Seta:(i : I.toSubtype) → (X i).toSubtype⊢ tuple a = tuple a sorryAll goals completed! 🐙

theorem declaration uses 'sorry'SetTheory.Set.tuple_symm {I:Set} {X: I → Set} (a b: ∀ i, X i) :
    tuple a = tuple b ↔ tuple b = tuple a := byinst✝:SetTheoryI:SetX:I.toSubtype → Seta:(i : I.toSubtype) → (X i).toSubtypeb:(i : I.toSubtype) → (X i).toSubtype⊢ tuple a = tuple b ↔ tuple b = tuple a sorryAll goals completed! 🐙

theorem declaration uses 'sorry'SetTheory.Set.tuple_trans {I:Set} {X: I → Set} {a b c: ∀ i, X i}
  (hab: tuple a = tuple b) (hbc : tuple b = tuple c) :
    tuple a = tuple c := byinst✝:SetTheoryI:SetX:I.toSubtype → Seta:(i : I.toSubtype) → (X i).toSubtypeb:(i : I.toSubtype) → (X i).toSubtypec:(i : I.toSubtype) → (X i).toSubtypehab:tuple a = tuple bhbc:tuple b = tuple c⊢ tuple a = tuple c sorryAll goals completed! 🐙

Вправа 3.5.4

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

Вправа 3.5.4

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

Вправа 3.5.4

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

Вправа 3.5.4

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

Вправа 3.5.4

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

Вправа 3.5.4

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

Вправа 3.5.5

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

/- Вправа 3.5.5 -/
def declaration uses 'sorry'SetTheory.Set.union_of_prod :
  Decidable (∀ (A B C D:Set), (A ×ˢ B) ∪ (C ×ˢ D) = (A ∪ C) ×ˢ (B ∪ D)) := byinst✝:SetTheory⊢ Decidable (∀ (A B C D : Set), A ×ˢ B ∪ C ×ˢ D = (A ∪ C) ×ˢ (B ∪ D))
  -- перший рядок цієї конструкції має бути `apply isTrue` або `apply isFalse`.
  sorryAll goals completed! 🐙

/- Вправа 3.5.5 -/
def declaration uses 'sorry'SetTheory.Set.diff_of_prod :
  Decidable (∀ (A B C D:Set), (A ×ˢ B) \ (C ×ˢ D) = (A \ C) ×ˢ (B \ D)) := byinst✝:SetTheory⊢ Decidable (∀ (A B C D : Set), A ×ˢ B \ C ×ˢ D = (A \ C) ×ˢ (B \ D))
  -- перший рядок цієї конструкції має бути `apply isTrue` або `apply isFalse`.
  sorryAll goals completed! 🐙

Вправа 3.5.6.

theorem declaration uses 'sorry'SetTheory.Set.prod_subset_prod {A B C D:Set}
  (hA: A ≠ ∅) (hB: B ≠ ∅) (hC: C ≠ ∅) (hD: D ≠ ∅) :
    A ×ˢ B ⊆ C ×ˢ D ↔ A ⊆ C ∧ B ⊆ D := byinst✝:SetTheoryA:SetB:SetC:SetD:SethA:A ≠ ∅hB:B ≠ ∅hC:C ≠ ∅hD:D ≠ ∅⊢ A ×ˢ B ⊆ C ×ˢ D ↔ A ⊆ C ∧ B ⊆ D sorryAll goals completed! 🐙

def declaration uses 'sorry'SetTheory.Set.prod_subset_prod' :
  Decidable (∀ (A B C D:Set), A ×ˢ B ⊆ C ×ˢ D ↔ A ⊆ C ∧ B ⊆ D) := byinst✝:SetTheory⊢ Decidable (∀ (A B C D : Set), A ×ˢ B ⊆ C ×ˢ D ↔ A ⊆ C ∧ B ⊆ D)
  -- перший рядок цієї конструкції має бути `apply isTrue` або `apply isFalse`.
  sorryAll goals completed! 🐙

Вправа 3.5.7

theorem declaration uses 'sorry'SetTheory.Set.direct_sum {X Y Z:Set} (f: Z → X) (g: Z → Y) :
    ∃! h: Z → X ×ˢ Y, fst ∘ h = f ∧ snd ∘ h = g := byinst✝:SetTheoryX:SetY:SetZ:Setf:Z.toSubtype → X.toSubtypeg:Z.toSubtype → Y.toSubtype⊢ ∃! h, fst ∘ h = f ∧ snd ∘ h = g sorryAll goals completed! 🐙

Вправа 3.5.8

@[simp]
theorem declaration uses 'sorry'SetTheory.Set.iProd_empty_iff {n:ℕ} {X: Fin n → Set} :
    iProd X = ∅ ↔ ∀ i, X i = ∅ := byinst✝:SetTheoryn:ℕX:(Fin n).toSubtype → Set⊢ iProd X = ∅ ↔ ∀ (i : (Fin n).toSubtype), X i = ∅ sorryAll goals completed! 🐙

Вправа 3.5.9

theorem declaration uses 'sorry'SetTheory.Set.iUnion_inter_iUnion {I J: Set} (A: I → Set) (B: J → Set) :
    (iUnion I A) ∩ (iUnion J B) = iUnion (I ×ˢ J) (fun p ↦ (A (fst p)) ∩ (B (snd p))) := byinst✝:SetTheoryI:SetJ:SetA:I.toSubtype → SetB:J.toSubtype → Set⊢ I.iUnion A ∩ J.iUnion B = (I ×ˢ J).iUnion fun p => A (fst p) ∩ B (snd p) sorryAll goals completed! 🐙

abbrev SetTheory.Set.graph {X Y:Set} (f: X → Y) : Set :=
  (X ×ˢ Y).specify (fun p ↦ (f (fst p) = snd p))

Вправа 3.5.10

theorem declaration uses 'sorry'SetTheory.Set.graph_inj {X Y:Set} (f f': X → Y) :
    graph f = graph f' ↔ f = f' := byinst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypef':X.toSubtype → Y.toSubtype⊢ graph f = graph f' ↔ f = f' sorryAll goals completed! 🐙

theorem declaration uses 'sorry'SetTheory.Set.is_graph {X Y G:Set} (hG: G ⊆ X ×ˢ Y)
  (hvert: ∀ x:X, ∃! y:Y, ((⟨x,y⟩:OrderedPair):Object) ∈ G) :
    ∃! f: X → Y, G = graph f := byinst✝:SetTheoryX:SetY:SetG:SethG:G ⊆ X ×ˢ Yhvert:∀ (x : X.toSubtype), ∃! y, OrderedPair.toObject { fst := ↑x, snd := ↑y } ∈ G⊢ ∃! f, G = graph f sorryAll goals completed! 🐙

Вправа 3.5.11. Це тривіально випливає з unknown identifier 'SetTheory.Set.power_set_axiom''SetTheory.Set.power_set_axiom', але вправа полягає у виведенні твердження з unknown identifier 'SetTheory.Set.mem_powerset'SetTheory.Set.mem_powerset.

theorem declaration uses 'sorry'SetTheory.Set.power_set_axiom' (X Y:Set) :
    ∃! S:Set, ∀(F:Object), F ∈ S ↔ ∃ f: Y → X, object_of f = F := sorry

Вправа 3.5.12, з включеними помилками з веб-сайту

theorem declaration uses 'sorry'SetTheory.Set.recursion (X: Type) (f: nat → X → X) (c:X) :
    ∃! a: nat → X, a 0 = c ∧ ∀ n, a (n + 1:ℕ) = f n (a n) := byinst✝:SetTheoryX:Typef:nat.toSubtype → X → Xc:X⊢ ∃! a, a 0 = c ∧ ∀ (n : ℕ), a ↑(n + 1) = f (↑n) (a ↑n) sorryAll goals completed! 🐙

Вправа 3.5.13

theorem declaration uses 'sorry'SetTheory.Set.nat_unique (nat':Set) (zero:nat') (succ:nat' → nat')
  (succ_ne: ∀ n:nat', succ n ≠ zero) (succ_of_ne: ∀ n m:nat', n ≠ m → succ n ≠ succ m)
  (ind: ∀ P: nat' → Prop, P zero → (∀ n, P n → P (succ n)) → ∀ n, P n) :
    ∃! f : nat → nat', Function.Bijective f ∧ f 0 = zero
    ∧ ∀ (n:nat) (n':nat'), f n = n' ↔ f (n+1:ℕ) = succ n' := byinst✝:SetTheorynat':Setzero:nat'.toSubtypesucc:nat'.toSubtype → nat'.toSubtypesucc_ne:∀ (n : nat'.toSubtype), succ n ≠ zerosucc_of_ne:∀ (n m : nat'.toSubtype), n ≠ m → succ n ≠ succ mind:∀ (P : nat'.toSubtype → Prop), P zero → (∀ (n : nat'.toSubtype), P n → P (succ n)) → ∀ (n : nat'.toSubtype), P n⊢ ∃! f,
  Function.Bijective f ∧
    f 0 = zero ∧ ∀ (n : nat.toSubtype) (n' : nat'.toSubtype), f n = n' ↔ f ↑(nat_equiv.symm n + 1) = succ n' sorryAll goals completed! 🐙

end Chapter3