expNear_sub — Mathlib

English

ExpNear as a function of r is affine in r: expNear(n, x, r1) − expNear(n, x, r2) = x^n/n! (r1 − r2).

Русский

ExpNear по аргументу r аффинна: expNear(n, x, r1) − expNear(n, x, r2) = x^n/n! (r1 − r2).

LaTeX

$$$\\operatorname{expNear}(n, x, r_{1}) - \\operatorname{expNear}(n, x, r_{2}) = \\frac{x^{n}}{n!} (r_{1} - r_{2}).$$$

Lean4

theorem expNear_sub (n x r₁ r₂) : expNear n x r₁ - expNear n x r₂ = x ^ n / n.factorial * (r₁ - r₂) := by
  simp [expNear, mul_sub]

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