Theorems · Theorem · logic and foundations

Ordinal.bsup_succ_of_mono

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

∀ {o : Ordinal.{u_3}} {f : (a : Ordinal.{u_3}) → a < Order.succ o → Ordinal.{max u_3 u_4}},
  (∀ {i j : Ordinal.{u_3}} (hi : i < Order.succ o) (hj : j < Order.succ o), i ≤ j → f i hi ≤ f j hj) →
    (Order.succ o).bsup f = f o ⋯

Defined in

Mathlib.SetTheory.Ordinal.Family

Cited by

1 results in Mathlib

Foundations

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