ext

Mathlib.Geometry.Manifold.VectorBundle.SmoothSection

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

English

Subtraction of smooth sections is smooth.

Русский

Вычитание гладких секций гладко.

LaTeX

$$$\text{ContMDiffSection.co e_sub}: s,t \mapsto s-t$ is smooth.$$

Lean4

@[ext]
theorem ext (h : ∀ x, s x = t x) : s = t :=
  DFunLike.ext _ _ h

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

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

Разделы

Аффилиация

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