Theorems · Theorem · order theory

zorn_subset_nonempty

∀ {α : Type u_1} (S : Set (Set α)),
  (∀ c ⊆ S, IsChain (fun x1 x2 => x1 ⊆ x2) c → c.Nonempty → ∃ ub ∈ S, ∀ s ∈ c, s ⊆ ub) →
    ∀ x ∈ S, ∃ m, x ⊆ m ∧ Maximal (fun x => x ∈ S) m

Defined in

Mathlib.Order.Zorn

Cited by

8 results in Mathlib

Foundations

Depth 70 from the axioms · uses propext, Classical.choice, Quot.sound