affineSpan_pair_le_of_mem_of_mem — Mathlib

English

The affine span of two points contained in a subspace is contained in that subspace.

Русский

Аффинная оболочка двух точек, принадлежащих подполнению, содержится в этом подполнении.

LaTeX

$$$\text{line}(k, p_1, p_2) \le s$ if $p_1\in s$ and $p_2\in s$.$$

Lean4

/-- The span of two points that lie in an affine subspace is contained in that subspace. -/
theorem affineSpan_pair_le_of_mem_of_mem {p₁ p₂ : P} {s : AffineSubspace k P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) :
    line[k, p₁, p₂] ≤ s :=
  by
  rw [affineSpan_le, Set.insert_subset_iff, Set.singleton_subset_iff]
  exact ⟨hp₁, hp₂⟩

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