Theorems · Theorem · logic and foundations

Ordinal.nfp_mul_opow_omega0_add

∀ {a c : Ordinal.{u_1}} (b : Ordinal.{u_1}),
  0 < a →
    0 < c →
      c ≤ a ^ Ordinal.omega0 →
        Ordinal.nfp (fun x => a * x) (a ^ Ordinal.omega0 * b + c) = a ^ Ordinal.omega0 * Order.succ b

Defined in

Mathlib.SetTheory.Ordinal.FixedPoint

Cited by

1 results in Mathlib

Foundations

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