Theorems · Theorem · logic and foundations

Ordinal.isNormal_enumOrd

∀ {s : Set Ordinal.{u}},
  (∀ t ⊆ s, t.Nonempty → BddAbove t → sSup t ∈ s) → ¬BddAbove s → Order.IsNormal (Ordinal.enumOrd s)

If s is closed under nonempty suprema, then its enumerator function is normal. See also enumOrd_isNormal_iff_isClosed.

Defined in

Mathlib.SetTheory.Ordinal.Enum

Cited by

0 results in Mathlib

Foundations

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