injective — Mathlib

English

A convex independent family is injective: equal values imply equal indices.

Русский

Конвексивно независимое семейство инъективно: равные значения означают равные индексы.

LaTeX

$$$\\text{ConvexIndependent}_{\\mathbb{k}}(p) \\rightarrow \\text{Function.Injective}(p)$$$

Lean4

/-- A convex independent family is injective. -/
protected theorem injective {p : ι → E} (hc : ConvexIndependent 𝕜 p) : Function.Injective p :=
  by
  refine fun i j hij => hc { j } i ?_
  rw [hij, Set.image_singleton, convexHull_singleton]
  exact Set.mem_singleton _

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