class WellOrder (α : Type u_1) extends TotalOrder α : Type u_1

• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a ≤ a
• le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
• le_total : ∀ (x y : α), Comparable x y
• existsLeast : ∀ {s : Set α}, s.Nonempty → ∃ (a : α), ∃ (h : a ∈ s), Least ⟨a, h⟩

noncomputable def WellOrder.least {α : Type u} [WellOrder α] {s : Set α} (h : s.Nonempty) : α

Equations

• WellOrder.least h = Classical.choose ⋯

@[simp]

theorem WellOrder.least_mem {α : Type u} [WellOrder α] {s : Set α} (h : s.Nonempty) : WellOrder.least h ∈ s

@[simp]

theorem WellOrder.least_least {α : Type u} [WellOrder α] {s : Set α} (h : s.Nonempty) {x : ↥s} : WellOrder.least h ≤ x.val

class IsWellOrder {α : Type u} (r : Relation α α) extends IsTotalOrder r : Prop

• le_refl : ∀ (a : α), (a, a) ∈ r
• le_trans : ∀ (a b c : α), (a, b) ∈ r → (b, c) ∈ r → (a, c) ∈ r
• le_antisymm : ∀ (a b : α), (a, b) ∈ r → (b, a) ∈ r → a = b
• le_total : ∀ (a b : α), (a, b) ∈ r ∨ (b, a) ∈ r
• existsLeast : ∀ {s : Set α}, s.Nonempty → ∃ (a : α), ∃ (_h : a ∈ s), ∀ (b : ↥s), (a, b.val) ∈ r

instance instWellOrderRelAsLEOfIsWellOrder {α : Type u} {r : Relation α α} [inst : IsWellOrder r] : WellOrder (RelAsLE r)

Equations

• instWellOrderRelAsLEOfIsWellOrder = WellOrder.mk ⋯

theorem WellOrder.isWellOrder {α : Type u} [WellOrder α] : IsWellOrder {p : α × α | p.fst ≤ p.snd}

noncomputable instance WellOrder.ne_has_least {α : Type u} [ne : Nonempty α] [WellOrder α] : HasLeast α

Equations

• WellOrder.ne_has_least = { least := ⋯.choose, least_le := ⋯ }

instance instWellOrderEmpty : WellOrder Empty

Equations

• instWellOrderEmpty = WellOrder.mk @instWellOrderEmpty.proof_1

instance instWellOrderUnit : WellOrder Unit

Equations

• instWellOrderUnit = WellOrder.mk @instWellOrderUnit.proof_1

instance instWellOrderSubtype {α : Type u} [WellOrder α] {p : α → Prop} : WellOrder { x : α // p x }

Equations

• instWellOrderSubtype = WellOrder.mk ⋯

instance instWellOrderAdjoinGreatest {α : Type u} [WellOrder α] : WellOrder (AdjoinGreatest α)

Equations

• instWellOrderAdjoinGreatest = WellOrder.mk ⋯

def totalOrder_of_exists_least {α : Type u} [PartialOrder α] (h : ∀ {s : Set α}, s.Nonempty → ∃ (a : α), ∃ (h : a ∈ s), Least ⟨a, h⟩) : TotalOrder α

Equations

• totalOrder_of_exists_least h = TotalOrder.mk ⋯

def IsOrderIso.wellOrder {α : Type u} {β : Type u_1} [WellOrder α] [Preorder β] {f : α → β} (h : IsOrderIso f) : WellOrder β

Equations

• h.wellOrder = WellOrder.mk ⋯

def WellOrder.carry_bij {α : Type u} [WellOrder α] {β : Type u_1} (f : Function.Bijection α β) : WellOrder β

Equations

• WellOrder.carry_bij f = WellOrder.mk ⋯

theorem WellOrder.hasLUB_of_bounded_above {α : Type u} [WellOrder α] {s : Set α} (h : s.BoundedAbove) : ∃ (x : α), IsLUB s x

theorem WellOrder.isIio_of_downwardsClosed {α : Type u} [WellOrder α] {s : Set α} (h : s.IsDownwardsClosed) (h' : s ≠ Set.univ) : ∃ (x : α), s = Set.Iio x

def WellOrder.InitialSegment (α : Type u) [WellOrder α] : Type u

Equations

• WellOrder.InitialSegment α = { s : Set α // s.IsDownwardsClosed }

def WellOrder.InitialSegment.mk {α : Type u} [WellOrder α] (a : α) : WellOrder.InitialSegment α

Equations

• WellOrder.InitialSegment.mk a = ⟨Set.Iio a, ⋯⟩

def WellOrder.InitialSegment.univ {α : Type u} [WellOrder α] : WellOrder.InitialSegment α

Equations

• WellOrder.InitialSegment.univ = ⟨Set.univ, ⋯⟩

noncomputable def WellOrder.InitialSegment.succ_mk {α : Type u} [WellOrder α] (a : α) : WellOrder.InitialSegment α

Equations

• WellOrder.InitialSegment.succ_mk a = ⟨Set.Iio a ∪ {a}, ⋯⟩

theorem WellOrder.InitialSegment.mk_inj {α : Type u} [WellOrder α] : Function.Injective WellOrder.InitialSegment.mk

@[simp]

theorem WellOrder.InitialSegment.univ_neq_mk {α : Type u} [WellOrder α] {a : α} : WellOrder.InitialSegment.univ ≠ WellOrder.InitialSegment.mk a

instance WellOrder.instPartialOrderInitialSegment {α : Type u} [WellOrder α] : PartialOrder (WellOrder.InitialSegment α)

Equations

• WellOrder.instPartialOrderInitialSegment = PartialOrder.mk ⋯

@[simp]

theorem WellOrder.InitialSegment.mk_le_mk_iff {α : Type u} [WellOrder α] {a b : α} : WellOrder.InitialSegment.mk a ≤ WellOrder.InitialSegment.mk b ↔ a ≤ b

@[simp]

theorem WellOrder.InitialSegment.le_univ {α : Type u} [WellOrder α] {a : WellOrder.InitialSegment α} : a ≤ WellOrder.InitialSegment.univ

theorem WellOrder.InitialSegment.univ_greatest {α : Type u} [WellOrder α] : Greatest WellOrder.InitialSegment.univ

theorem WellOrder.InitialSegment.mk_or_univ {α : Type u} [WellOrder α] (i : WellOrder.InitialSegment α) : (∃ (a : α), i = WellOrder.InitialSegment.mk a) ∨ i = WellOrder.InitialSegment.univ

@[simp]

theorem WellOrder.InitialSegment.mk_lt_succ_mk {α : Type u} [WellOrder α] {a : α} : WellOrder.InitialSegment.mk a < WellOrder.InitialSegment.succ_mk a

instance WellOrder.instTotalOrderInitialSegment {α : Type u} [WellOrder α] : TotalOrder (WellOrder.InitialSegment α)

Equations

• WellOrder.instTotalOrderInitialSegment = TotalOrder.mk ⋯

def WellOrder.InitialSegment.adjoinGreatest_iso {α : Type u} [WellOrder α] : AdjoinGreatest α → WellOrder.InitialSegment α

Equations

• WellOrder.InitialSegment.adjoinGreatest_iso (Sum.inr val) = WellOrder.InitialSegment.univ
• WellOrder.InitialSegment.adjoinGreatest_iso (Sum.inl a) = WellOrder.InitialSegment.mk a

theorem WellOrder.InitialSegment.adjoinGreatest_iso_is_iso {α : Type u} [WellOrder α] : IsOrderIso WellOrder.InitialSegment.adjoinGreatest_iso

theorem WellOrder.InitialSegment.univ_val_isOrderIso {α : Type u} [WellOrder α] : IsOrderIso Subtype.val

theorem WellOrder.InitialSegment.mk_unit_isOrderIso {α : Type u} [WellOrder α] : IsOrderIso fun (x : α) => ⟨x, True.intro⟩

instance WellOrder.instInitialSegment {α : Type u} [WellOrder α] : WellOrder (WellOrder.InitialSegment α)

Equations

• WellOrder.instInitialSegment = ⋯.wellOrder

instance WellOrder.instIsDownwardsClosedValSet {α : Type u} [WellOrder α] {a : WellOrder.InitialSegment α} : a.val.IsDownwardsClosed

Equations

• ⋯ = ⋯

theorem WellOrder.InitialSegment.induction {α : Type u} [WellOrder α] {p : WellOrder.InitialSegment α → Prop} {x : WellOrder.InitialSegment α} (h_union : ∀ (ι : Type u) (f : ι → WellOrder.InitialSegment α), (∀ (i : ι), p (f i)) → p ⟨⋃ i : ι, (f i).val, ⋯⟩) (h_succ : ∀ (a : α), p (WellOrder.InitialSegment.mk a) → p (WellOrder.InitialSegment.succ_mk a)) : p x

theorem WellOrder.wf_induction {α : Type u} [WellOrder α] {p : α → Prop} (h : ∀ (x : α), (∀ (y : α), y < x → p y) → p x) (x : α) : p x

theorem WellOrder.wf_recursion_all_eq {α : Type u} [WellOrder α] {p : α → Type u_1} {f g : (x : α) → p x} (h : (x : α) → ((y : α) → y < x → p y) → p x) (eqf : ∀ (x : α), (h x fun (y : α) (x : y < x) => f y) = f x) (eqg : ∀ (x : α), (h x fun (y : α) (x : y < x) => g y) = g x) : f = g

theorem WellOrder.wf_recursion_exists {α : Type u} [WellOrder α] {p : α → Type u_1} (h : (x : α) → ((y : α) → y < x → p y) → p x) : ∃ (f : (x : α) → p x), ∀ (x : α), f x = h x fun (y : α) (x : y < x) => f y

noncomputable def WellOrder.wf_recursion {α : Type u} [WellOrder α] {p : α → Type u_1} (h : (x : α) → ((y : α) → y < x → p y) → p x) (x : α) : p x

Equations

• WellOrder.wf_recursion h = Classical.choose ⋯

theorem WellOrder.wf_recursion_eq {α : Type u} [WellOrder α] {p : α → Type u_1} (h : (x : α) → ((y : α) → y < x → p y) → p x) (x : α) : WellOrder.wf_recursion h x = h x fun (y : α) (x : y < x) => WellOrder.wf_recursion h y

def WellOrder.InitialSegment.lift_double {α : Type u} [WellOrder α] {x : WellOrder.InitialSegment α} (y : WellOrder.InitialSegment ↥x.val) : WellOrder.InitialSegment α

Equations

• WellOrder.InitialSegment.lift_double y = ⟨Subtype.val '' y.val, ⋯⟩

@[simp]

theorem WellOrder.InitialSegment.lift_double_val {α : Type u} [WellOrder α] {x : WellOrder.InitialSegment α} (y : WellOrder.InitialSegment ↥x.val) : (WellOrder.InitialSegment.lift_double y).val = Subtype.val '' y.val

@[simp]

theorem WellOrder.InitialSegment.lift_double_mono {α : Type u} [WellOrder α] {x : WellOrder.InitialSegment α} : Monotone WellOrder.InitialSegment.lift_double

theorem WellOrder.InitialSegment.lift_double_iso {α : Type u} [WellOrder α] {x : WellOrder.InitialSegment α} (y : WellOrder.InitialSegment ↥x.val) : ∃ (f : ↥y.val → ↥(WellOrder.InitialSegment.lift_double y).val), IsOrderIso f

@[simp]

theorem WellOrder.InitialSegment.lift_double_le {α : Type u} [WellOrder α] {x : WellOrder.InitialSegment α} (y : WellOrder.InitialSegment ↥x.val) : WellOrder.InitialSegment.lift_double y ≤ x

instance ZermeloTheorem.isWellOrderColimit {α : Type u} {ι : Type u_1} {x : ι → Set α} [RightDirected ↥(x '' Set.univ)] (h : Set.IsCovering x) {f : (i : ι) → Relation ↥(x i) ↥(x i)} [inst : ∀ (i : ι), IsWellOrder (f i)] (h' : ∀ (i j : ι) (sub : x i ⊆ x j) (a b : α) (ha : a ∈ x i) (hb : b ∈ x i), (⟨a, ha⟩, ⟨b, hb⟩) ∈ f i ↔ (⟨a, ⋯⟩, ⟨b, ⋯⟩) ∈ f j) (h'' : ∀ (i j : ι) (sub : x i ⊆ x j) (a b : α) (ha : a ∈ x i) (hb : b ∈ x j), (⟨b, hb⟩, ⟨a, ⋯⟩) ∈ f j → b ∈ x i) (h''' : ∀ (i j : ι), x i ⊆ x j ∨ x j ⊆ x i) : IsWellOrder (h.glue_rel f)

Equations

• ⋯ = ⋯

structure ZermeloTheorem.PartialWellOrder (α : Type u_1) (s : Set (Set α)) (p : ↥s → α) : Type u_1

• domain : Set α
• order : WellOrder ↥self.domain
• iic_mem : ∀ (x : ↥self.domain), {x_1 : α | ∃ (a : ↥self.domain), a ∈ Set.Iic x ∧ a.val = x_1} ∈ s
• iic_func : ∀ (x : ↥self.domain), p ⟨{x_1 : α | ∃ (a : ↥self.domain), a ∈ Set.Iic x ∧ a.val = x_1}, ⋯⟩ = x.val
• domain_not_mem : ¬self.domain ∈ s

def ZermeloTheorem.make_partialWellOrder {α : Type u} {s : Set (Set α)} (p : ↥s → α) (hf : ∀ (a : ↥s), ¬p a ∈ a.val) : ZermeloTheorem.PartialWellOrder α s p

Equations

• ZermeloTheorem.make_partialWellOrder p hf = sorry

def ZermeloTheorem.zermelo {α : Type u} : WellOrder α

Equations

• zermelo = WellOrder.carry_bij Function.bijection_univ