affineSpan_pair_le_of_right_mem — Mathlib

English

If p lies in the affine span of ps, inserting p into ps does not change the span.

Русский

Если p принадлежит аффинной оболочке ps, добавление p в ps не изменяет оболочку.

LaTeX

$$$p \in \operatorname{affineSpan}(k, ps) \Rightarrow \operatorname{affineSpan}(k, \operatorname{insert } p ps) = \operatorname{affineSpan}(k, ps).$$$

Lean4

/-- One line is contained in another differing in the second point if the second point of the
first line is contained in the second line. -/
theorem affineSpan_pair_le_of_right_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 (left_mem_affineSpan_pair _ _ _) h

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