approximatesLinearOn_empty — Mathlib

English

If ApproximatesLinearOn holds, then f − f' is Lipschitz on s with a bound c.

Русский

Если выполняется ApproximatesLinearOn, то разность f − f' является Липшицевой на s с пределом c.

LaTeX

$$$\text{ApproximatesLinearOn}(f,f',s,c) \implies \text{LipschitzOnWith}(c)(f - f')\;\text{на } s$$$

Lean4

@[simp]
theorem approximatesLinearOn_empty (f : E → F) (f' : E →L[𝕜] F) (c : ℝ≥0) : ApproximatesLinearOn f f' ∅ c := by
  simp [ApproximatesLinearOn]

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