lineMap_rev_mem_affineSpan_pair — Mathlib

English

The reversed lineMap lies in the affine span of the two points.

Русский

Обратный lineMap принадлежит афинному охвату двух точек.

LaTeX

$$$\\operatorname{AffineMap.lineMap}(p_2,p_1,r) \\in \\mathrm{line}[k, p_1, p_2]$$$

Lean4

/-- A combination of two points expressed with `lineMap` (with the two points reversed) lies in
their affine span. -/
theorem lineMap_rev_mem_affineSpan_pair (r : k) (p₁ p₂ : P) : AffineMap.lineMap p₂ p₁ r ∈ line[k, p₁, p₂] :=
  AffineMap.lineMap_mem _ (right_mem_affineSpan_pair _ _ _) (left_mem_affineSpan_pair _ _ _)

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