differentiable — Mathlib

English

Extensionality lemma for Schwartz maps: f=g if they agree pointwise.

Русский

Кнопка экстенсиональности для отображений Шварца: f=g, если они равны на каждой точке.

LaTeX

$$$ \forall f,g : \mathcal{S}(E,F),\ (\forall x, f(x)=g(x)) \Rightarrow f=g$$$

Lean4

/-- Every Schwartz function is differentiable. -/
protected theorem differentiable (f : 𝓢(E, F)) : Differentiable ℝ f :=
  (f.smooth 1).differentiable rfl.le

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