affineSpan_pair_le_of_left_mem — Mathlib

English

The affine span of a point added to the span is the same as adding the point to the base set and spanning.

Русский

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

LaTeX

$$$\operatorname{affineSpan}(k, (\text{insert } p (\operatorname{affineSpan}(k, ps) : \text{Set} P))) = \operatorname{affineSpan}(k, \text{insert } p ps).$$$

Lean4

/-- One line is contained in another differing in the first point if the first point of the first
line is contained in the second line. -/
theorem affineSpan_pair_le_of_left_mem {p₁ p₂ p₃ : P} (h : p₁ ∈ line[k, p₂, p₃]) : line[k, p₁, p₃] ≤ line[k, p₂, p₃] :=
  affineSpan_pair_le_of_mem_of_mem h (right_mem_affineSpan_pair _ _ _)

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