class InductiveOrder (α : Type u_1) [PartialOrder α] : Prop

• chain_boundedAbove : ∀ {s : Set α}, (∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → Comparable x y) → s.BoundedAbove

instance instInductiveOrderSet {α : Type u_1} : InductiveOrder (Set α)

Equations

• ⋯ = ⋯

instance instInductiveOrderSubtypeMemSetIci {α : Type u_1} [PartialOrder α] [InductiveOrder α] {a : α} : InductiveOrder ↥(Set.Ici a)

Equations

• ⋯ = ⋯

noncomputable def PartialMap.iUnion {α : Type u_1} {β : α → Type u_2} {ι : Type u_3} (f : ι → PartialMap α β) : PartialMap α β

Equations

• PartialMap.iUnion f = { carrier := ⋃ i : ι, (f i).carrier, function := fun (x : ↥(⋃ i : ι, (f i).carrier)) => (f (Classical.choose ⋯)).function ⟨x.val, ⋯⟩ }

@[simp]

theorem PartialMap.iUnion_lub {α : Type u_1} {β : α → Type u_2} {ι : Type u_3} {f : ι → PartialMap α β} (h : ∀ (i j : ι), Comparable (f i) (f j)) : IsLUB (f '' Set.univ) (PartialMap.iUnion f)

instance instInductiveOrderPartialMap {α : Type u_1} {β : α → Type u_2} : InductiveOrder (PartialMap α β)

Equations

• ⋯ = ⋯

theorem wellOrder_bounded_above_has_maximal {α : Type u_1} [PartialOrder α] (h : ∀ {s : Set α}, IsWellOrder {(x, y) : ↥s × ↥s | x.val ≤ y.val} → s.BoundedAbove) : ∃ (x : α), Maximal x

theorem InductiveOrder.has_maximal {α : Type u_1} [PartialOrder α] [InductiveOrder α] : ∃ (x : α), Maximal x

zorns lemma

theorem InductiveOrder.has_maximal_above {α : Type u_1} [PartialOrder α] [InductiveOrder α] (a : α) : ∃ (x : α), Maximal x ∧ x ≥ a

theorem subset_chain_iUnion_inductive {α : Type u_1} {s : Set (Set α)} (h1 : s.Nonempty) (h : ∀ (t : Set (Set α)), t.Nonempty → t ⊆ s → (∀ (x : Set α), x ∈ t → ∀ (y : Set α), y ∈ t → x ⊆ y ∨ y ⊆ x) → ⋃ a : ↥t, a.val ∈ s) : InductiveOrder ↥s

theorem subset_totally_ordered_maximum {α : Type u_1} {s : Set (Set α)} (h1 : s.Nonempty) (h : ∀ (t : Set (Set α)), t.Nonempty → t ⊆ s → (∀ (x : Set α), x ∈ t → ∀ (y : Set α), y ∈ t → x ⊆ y ∨ y ⊆ x) → ⋃ a : ↥t, a.val ∈ s) : ∃ (x : ↥s), Maximal x

theorem subset_totally_ordered_minimum {α : Type u_1} {s : Set (Set α)} (h1 : s.Nonempty) (h : ∀ (t : Set (Set α)), t.Nonempty → t ⊆ s → (∀ (x : Set α), x ∈ t → ∀ (y : Set α), y ∈ t → x ⊆ y ∨ y ⊆ x) → ⋂ a : ↥t, a.val ∈ s) : ∃ (x : ↥s), Minimal x