deriv_add_eq_mul_omega0_add — Mathlib

English

deriv (a + ·) b = a · ω + b.

Русский

deriv (a + ·) b = a · ω + b.

LaTeX

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

Lean4

theorem deriv_add_eq_mul_omega0_add (a b : Ordinal.{u}) : deriv (a + ·) b = a * ω + b :=
  by
  revert b
  rw [← funext_iff, IsNormal.eq_iff_zero_and_succ (isNormal_deriv _) (isNormal_add_right _)]
  refine ⟨?_, fun a h => ?_⟩
  · rw [deriv_zero_right, add_zero]
    exact nfp_add_zero a
  · rw [deriv_succ, h, add_succ]
    exact nfp_eq_self (add_eq_right_iff_mul_omega0_le.2 ((le_add_right _ _).trans (le_succ _)))

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