lineMap_toAffineMap — Mathlib

English

The affine part of the lineMap coincides with the usual lineMap in Affine geometry.

Русский

Аффинная часть lineMap совпадает с обычной lineMap в аффинной геометрии.

LaTeX

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

Lean4

@[simp]
theorem lineMap_toAffineMap (p₀ p₁ : P) [TopologicalSpace R] [TopologicalSpace V] [ContinuousSMul R V]
    [ContinuousVAdd V P] : (lineMap p₀ p₁).toAffineMap = AffineMap.lineMap (k := R) p₀ p₁ :=
  rfl

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