subset — Mathlib

English

A subset of a collinear set is collinear.

Русский

Подмножество коллинеарного множества коллинеарно.

LaTeX

$$$\text{If } s_1 \subseteq s_2 \text{ and } \operatorname{Collinear}_k(s_2), \text{ then } \operatorname{Collinear}_k(s_1).$$$

Lean4

/-- A subset of a collinear set is collinear. -/
theorem subset {s₁ s₂ : Set P} (hs : s₁ ⊆ s₂) (h : Collinear k s₂) : Collinear k s₁ :=
  (Submodule.rank_mono (vectorSpan_mono k hs)).trans h

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