Theorems · Theorem · logic and foundations

Ordinal.CNF.eval_add

∀ (b : Ordinal.{u_1}) {f₁ f₂ : Ordinal.{u_1} →₀ Ordinal.{u_1}},
  (∀ e₁ ∈ f₁.support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁) →
    Ordinal.CNF.eval b (f₁ + f₂) = Ordinal.CNF.eval b f₁ + Ordinal.CNF.eval b f₂

Defined in

Mathlib.SetTheory.Ordinal.CantorNormalForm

Cited by

0 results in Mathlib

Foundations

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