mem_affineSpan_singleton — Mathlib

English

For any p1 and p2 in space P, p1 belongs to the affine span of {p2} if and only if p1 = p2.

Русский

Любая точка p1 принадлежит аффинному охвату множества {p2} тогда и только тогда, когда p1 = p2.

LaTeX

$$$ p_1 \\in affineSpan_k(\\{p_2\\}) \\iff p_1 = p_2 $$$

Lean4

/-- A point is in the affine span of a single point if and only if they are equal. -/
@[simp]
theorem mem_affineSpan_singleton : p₁ ∈ affineSpan k ({ p₂ } : Set P) ↔ p₁ = p₂ := by simp [← mem_coe]

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