Theorems · Theorem · logic and foundations

Ordinal.CNF.foldr

∀ (b o : Ordinal.{u_1}), List.foldr (fun p r => b ^ p.1 * p.2 + r) 0 (Ordinal.CNF b o) = o

Evaluating the Cantor normal form of an ordinal returns the ordinal.

Defined in

Mathlib.SetTheory.Ordinal.CantorNormalForm

Cited by

1 results in Mathlib

Foundations

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