subtype — Mathlib

English

A convex independent family remains convex independent when restricted to any subset via subtype.

Русский

При ограничении семейства до подмножества через субтип независимость сохраняется.

LaTeX

$$$\\text{ConvexIndependent}_{\\mathbb{k}}(p) \\Rightarrow \\forall s,\\; \\text{ConvexIndependent}_{\\mathbb{k}}(p|_{s})$$$

Lean4

/-- If a family is convex independent, so is any subfamily indexed by a subtype of the index type.
-/
protected theorem subtype {p : ι → E} (hc : ConvexIndependent 𝕜 p) (s : Set ι) : ConvexIndependent 𝕜 fun i : s => p i :=
  hc.comp_embedding (Embedding.subtype _)

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