Theorems · Theorem · logic and foundations

Cardinal.blsub_lt_ord_lift_of_isRegular

Deprecated since 2026-03-22Use Ordinal.lift_iSup_add_one_lt_of_lt_cof instead.

∀ {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}} {c : Cardinal.{max u v}},
  c.IsRegular → Cardinal.lift.{v, u} o.card < c → (∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c.ord) → o.blsub f < c.ord

Defined in

Mathlib.SetTheory.Cardinal.Regular

Cited by

0 results in Mathlib

Foundations

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