const_contLinear

Mathlib.Topology.Algebra.ContinuousAffineMap

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

English

The lineMap from p0 to p1 has the same affine map as the standard lineMap with base field k := R.

Русский

LineMap от p0 до p1 имеет ту же аффинную карту, что стандартная lineMap с основанием k := R.

LaTeX

$$$\text{lineMap}(p_0,p_1) = \text{AffineMap.lineMap}(k:=R)(p_0,p_1)$$$

Lean4

@[simp]
theorem const_contLinear (q : Q) : (const R P q).contLinear = 0 :=
  rfl

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

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

Разделы

Аффилиация

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