const

Mathlib.Topology.Algebra.ContinuousAffineMap

URI: https://scilib.ai/kg/mathlib#ContinuousAffineMap.const

English

The linear part of the constant affine map is zero; i.e., its contLinear is the zero map.

Русский

Линейная часть константной аффинной карты равна нулю; contLinear — нулевая отображение.

LaTeX

$$$\text{const}(q)\!\!\text{contLinear} = 0$$$

Lean4

/-- The constant map as a continuous affine map -/
def const (q : Q) : P →ᴬ[R] Q :=
  { AffineMap.const R P q with cont := continuous_const }

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

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

Разделы

Аффилиация

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