instSub

Mathlib.Geometry.Manifold.VectorBundle.SmoothSection

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

English

nsmul (natural scalar multiplication) of a smooth section is smooth.

Русский

Умножение секции на натуральное число сохраняет гладкость.

LaTeX

$$$\text{ContMDiffSection.instNSMul}: (k \in \mathbb{N}) \cdot s \text{ smooth}.$$$

Lean4

instance instSub : Sub Cₛ^n⟮I; F, V⟯ :=
  ⟨fun s t ↦ ⟨s - t, s.contMDiff.sub_section t.contMDiff⟩⟩

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

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

Разделы

Аффилиация

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