secondInter_vsub_mem_affineSpan — Mathlib

English

The value s.secondInter(p1, p2 − p1) lies in the affine span of p1 and p2.

Русский

Значение s.secondInter(p1, p2 − p1) принадлежит аффинному пространству, порождённому p1 и p2.

LaTeX

$$$s.secondInter(p_1, p_2 - p_1) \\in \\mathrm{line}[\\mathbb{R}, p_1, p_2]$$$

Lean4

/-- If the vector passed to `secondInter` is given by a subtraction involving the point in
`secondInter`, the result lies in the span of the two points. -/
theorem secondInter_vsub_mem_affineSpan (s : Sphere P) (p₁ p₂ : P) : s.secondInter p₁ (p₂ -ᵥ p₁) ∈ line[ℝ, p₁, p₂] :=
  smul_vsub_vadd_mem_affineSpan_pair _ _ _

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