inhabited

Mathlib.Geometry.Manifold.VectorBundle.SmoothSection

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

English

The pointwise addition of smooth sections is smooth.

Русский

Пусть двух гладких секций суммируются по точкам — результат гладкий.

LaTeX

$$$\text{instAdd}$: $(s,t) \mapsto (x \mapsto s(x)+t(x))$ is ContMDiff.$$

Lean4

instance inhabited : Inhabited Cₛ^n⟮I; F, V⟯ :=
  ⟨0⟩

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

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

Разделы

Аффилиация

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