affineSpan_mono — Mathlib

English

Affine span is monotone with respect to set inclusion: if s1 ⊆ s2, then affineSpan(k, s1) ≤ affineSpan(k, s2).

Русский

Аффинная оболочка монотонна по включению множеств: если s1 ⊆ s2, то affineSpan(k, s1) ≤ affineSpan(k, s2).

LaTeX

$$$s_1 \subseteq s_2 \Rightarrow \operatorname{affineSpan}(k, s_1) \le \operatorname{affineSpan}(k, s_2).$$$

Lean4

/-- `affineSpan` is monotone. -/
@[gcongr, mono]
theorem affineSpan_mono {s₁ s₂ : Set P} (h : s₁ ⊆ s₂) : affineSpan k s₁ ≤ affineSpan k s₂ :=
  affineSpan_le_of_subset_coe (Set.Subset.trans h (subset_affineSpan k _))

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