Theorems · Theorem · logic and foundations

Ordinal.blsub_comp

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

∀ {o o' : Ordinal.{max u v}} {f : (a : Ordinal.{max u v}) → a < o → Ordinal.{max u v w}},
  (∀ {i j : Ordinal.{max u v}} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj) →
    ∀ {g : (a : Ordinal.{max u v}) → a < o' → Ordinal.{max u v}} (hg : o'.blsub g = o),
      (o'.blsub fun a ha => f (g a ha) ⋯) = o.blsub f

Defined in

Mathlib.SetTheory.Ordinal.Family

Cited by

2 results in Mathlib

Foundations

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