Theorems · Theorem · logic and foundations

Ordinal.blsub_le_iff

Deprecated since 2026-03-23Mathlib marks this declaration as deprecated.

∀ {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}} {a : Ordinal.{max u v}},
  o.blsub 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 84 from the axioms · uses propext, Classical.choice, Quot.sound