coe_lineMap_eq — Mathlib

English

The function underlying ContinuousAffineMap.lineMap equals the corresponding affine lineMap function.

Русский

Функция, лежащая в основе ContinuousAffineMap.lineMap, равна соответствующей функции линейной карты.

LaTeX

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

Lean4

theorem coe_lineMap_eq (p₀ p₁ : P) [TopologicalSpace R] [TopologicalSpace V] [ContinuousSMul R V] [ContinuousVAdd V P] :
    ⇑(ContinuousAffineMap.lineMap p₀ p₁) = ⇑(AffineMap.lineMap (k := R) p₀ p₁) :=
  rfl

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