nfp_mul_one — Mathlib

English

If 0 < a, then nfp (a · ·) 1 = a^ω.

Русский

Если 0 < a, то nfp (a · x) 1 = a^ω.

LaTeX

$$$$ \forall a > 0, \operatorname{nfp}(a \cdot \cdot) 1 = a^{\omega} $$$$

Lean4

@[simp]
theorem nfp_mul_one {a : Ordinal} (ha : 0 < a) : nfp (a * ·) 1 = a ^ ω :=
  by
  rw [← iSup_iterate_eq_nfp, ← iSup_pow ha]
  congr
  funext n
  induction n with
  | zero => rw [pow_zero, iterate_zero_apply]
  | succ n hn => rw [iterate_succ_apply', Nat.add_comm, pow_add, pow_one, hn]

Похожие утверждения