comp_embedding — Mathlib

English

If a family is convex independent, composing it with an embedding yields a convex independent family.

Русский

Если семейство выпукво независимо, композиция с вложением сохраняет независимость.

LaTeX

$$$\\text{ConvexIndependent}_{\\mathbb{k}}(p) \\Rightarrow \\text{ConvexIndependent}_{\\mathbb{k}}(p \\circ f)$, where $f: \\iota' \\hookrightarrow \\iota$ is an embedding.$$

Lean4

/-- If a family is convex independent, so is any subfamily given by composition of an embedding into
index type with the original family. -/
theorem comp_embedding {ι' : Type*} (f : ι' ↪ ι) {p : ι → E} (hc : ConvexIndependent 𝕜 p) :
    ConvexIndependent 𝕜 (p ∘ f) := by
  intro s x hx
  rw [← f.injective.mem_set_image]
  exact hc _ _ (by rwa [Set.image_image])

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