Minimal_Element_of_an_Ordinal
Provedordinalsproofwikiset-theory
The minimal element of any nonempty ordinal is the empty set. That is, if is a nonempty ordinal,
Preamble
import Mathlib.SetTheory.Ordinal.Basic
Formal statement
theorem Minimal_Element_of_an_Ordinal (o : Ordinal) (ho : o ≠ 0) : ∃ (a : Ordinal), a < o ∧ ∀ b, b < o → a ≤ b := by sorry
Source