mono — Mathlib

English

A subset of a convex independent set is convex independent.

Русский

Подмножество выпукво независимого множества тоже выпукво независимо.

LaTeX

$$$\\text{ConvexIndependent}_{\\mathbb{k}}(\\iota) \\to (s \\subseteq t) \\Rightarrow \\text{ConvexIndependent}_{\\mathbb{k}}(\\text{val} : s \\to E)$$$

Lean4

/-- A subset of a convex independent set of points is convex independent as well. -/
protected theorem mono {s t : Set E} (hc : ConvexIndependent 𝕜 ((↑) : t → E)) (hs : s ⊆ t) :
    ConvexIndependent 𝕜 ((↑) : s → E) :=
  hc.comp_embedding (s.embeddingOfSubset t hs)

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