nfp_mul_zero — Mathlib

English

For a > 0 and b ≤ a^ω, nfp (x ↦ a · x) b = a^ω.

Русский

Пусть b > 0 и b ≤ a^ω; тогда nfp (x ↦ a · x) b = a^ω.

LaTeX

$$$$ (0 < b) \land (b \le a^{\omega}) \Rightarrow \operatorname{nfp}(\lambda x. a \cdot x) b = a^{\omega} $$$$

Lean4

@[simp]
theorem nfp_mul_zero (a : Ordinal) : nfp (a * ·) 0 = 0 :=
  by
  rw [← Ordinal.le_zero, nfp_le_iff]
  intro n
  induction n with
  | zero => rfl
  | succ n hn => dsimp only; rwa [iterate_succ_apply, mul_zero]

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