nfp_add_eq_mul_omega0 — Mathlib

English

If b ≤ a + ω, then nfp (a + ·) b = a · ω when b ≤ a · ω.

Русский

Если b ≤ a + ω и b ≤ a · ω, то nfp (a + ·) b = a · ω.

LaTeX

$$$$ b \le a \cdot \omega \Rightarrow \operatorname{nfp}(\lambda x. a + x) b = a \cdot \omega $$$$

Lean4

theorem nfp_add_eq_mul_omega0 {a b} (hba : b ≤ a * ω) : nfp (a + ·) b = a * ω :=
  by
  apply le_antisymm (nfp_le_fp (isNormal_add_right a).monotone hba _)
  · rw [← nfp_add_zero]
    exact nfp_monotone (isNormal_add_right a).monotone (Ordinal.zero_le b)
  · dsimp; rw [← mul_one_add, one_add_omega0]

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