coe_injective

Mathlib.Geometry.Manifold.VectorBundle.SmoothSection

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

English

Addition of smooth sections is smooth.

Русский

Сложение гладких секций даёт гладкую секцию.

LaTeX

$$$\text{ContMDiffSection.instAdd}: s,t \mapsto s+t$ is smooth.$$

Lean4

theorem coe_injective : Injective ((↑) : Cₛ^n⟮I; F, V⟯ → ∀ x, V x) :=
  coe_inj

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

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

Разделы

Аффилиация

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