coplanar_insert_iff_of_mem_affineSpan

English

Inserting a point into a subspace increases the dimension of its vectorSpan by at most 1.

Русский

Добавление точки в подпространство увеличивает размерность vectorSpan не более чем на 1.

LaTeX

$$finrank_k(vectorSpan_k(insert p s)) ≤ finrank_k(s.direction) + 1$$

Lean4

/-- Adding a point in the affine span of a set does not change whether that set is coplanar. -/
theorem coplanar_insert_iff_of_mem_affineSpan {s : Set P} {p : P} (h : p ∈ affineSpan k s) :
    Coplanar k (insert p s) ↔ Coplanar k s := by rw [Coplanar, Coplanar, vectorSpan_insert_eq_vectorSpan h]

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