Theorems · Theorem · logic and foundations

Ordinal.veblenWith_veblenWith_of_lt

∀ {f : Ordinal.{u} → Ordinal.{u}} {o₁ o₂ : Ordinal.{u}},
  Order.IsNormal f →
    o₁ < o₂ → ∀ (a : Ordinal.{u}), Ordinal.veblenWith f o₁ (Ordinal.veblenWith f o₂ a) = Ordinal.veblenWith f o₂ a

Defined in

Mathlib.SetTheory.Ordinal.Veblen

Cited by

9 results in Mathlib

Foundations

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