Theorems · Theorem · logic and foundations

Ordinal.bsup_le_iff

Deprecated since 2026-04-05Mathlib marks this declaration as deprecated.

∀ {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}} {a : Ordinal.{max u v}},
  o.bsup f ≤ a ↔ ∀ (i : Ordinal.{u}) (h : i < o), f i h ≤ a

Defined in

Mathlib.SetTheory.Ordinal.Family

Cited by

4 results in Mathlib

Foundations

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