ext

Mathlib.Analysis.Distribution.SchwartzSpace

URI: https://scilib.ai/kg/mathlib#SchwartzMap.ext

English

Extensionality lemma for Schwartz maps (alternate labeling).

Русский

Экстенсиональность для Schwartz отображений (альтернативная нотация).

LaTeX

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

Lean4

@[ext]
theorem ext {f g : 𝓢(E, F)} (h : ∀ x, (f : E → F) x = g x) : f = g :=
  DFunLike.ext f g h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru