eqOn_dslope_sub_smul — Mathlib

English

For every a ∈ 𝕜, the function b ↦ dslope (x ↦ (x − a) f(x)) a b coincides with f(b) for all b ≠ a.

Русский

Для каждого a ∈ 𝕜 функция b ↦ dslope (x ↦ (x − a) f(x)) a b совпадает с f(b) для всех b ≠ a.

LaTeX

$$$\text{EqOn}\left( dslope\left( x \mapsto (x - a) \cdot f(x) \right)\ a \right) f\ ({a})^{\complement}$$$

Lean4

theorem eqOn_dslope_sub_smul (f : 𝕜 → E) (a : 𝕜) : EqOn (dslope (fun x => (x - a) • f x) a) f { a }ᶜ := fun _ =>
  dslope_sub_smul_of_ne f

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