convexIndependent_iff_set — Mathlib

English

For injective p, convex independence of the range map is equivalent to the convex independence of p.

Русский

Для инъективного p независимость диапазона седержится эквивалентно независимости p.

LaTeX

$$$\\text{Injective}(p) \\Rightarrow (\\text{ConvexIndependent}_{\\mathbb{k}}((\\uparrow):\\mathrm{range}(p)\\to E) \\;\\Leftrightarrow\\; \\text{ConvexIndependent}_{\\mathbb{k}}(p))$$$

Lean4

/-- The range of an injective indexed family of points is convex independent iff that family is. -/
theorem convexIndependent_iff_set {p : ι → E} (hi : Function.Injective p) :
    ConvexIndependent 𝕜 ((↑) : Set.range p → E) ↔ ConvexIndependent 𝕜 p :=
  ⟨fun hc =>
    hc.comp_embedding
      (⟨fun i => ⟨p i, Set.mem_range_self _⟩, fun _ _ h => hi (Subtype.mk_eq_mk.1 h)⟩ : ι ↪ Set.range p),
    ConvexIndependent.range⟩

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