convexIndependent_set_iff_inter_convexHull_subset

English

A subfamily is convex independent iff, for every subset t ⊆ s, we have s ∩ convHull t ⊆ t.

Русский

Подсемейство конвексивно независимо тогда и только тогда, когда для каждого подмножества t ⊆ s верно t, если пересечение s и convHull t принадлежит t.

LaTeX

$$$\\text{ConvexIndependent}_{\\mathbb{k}}((\\uparrow):s\\to E) \\;\\Leftrightarrow\\; \\forall t\\subseteq s,\\; s \\cap convHull_{\\mathbb{k}}(t) \\subseteq t$$$

Lean4

theorem convexIndependent_set_iff_inter_convexHull_subset {s : Set E} :
    ConvexIndependent 𝕜 ((↑) : s → E) ↔ ∀ t, t ⊆ s → s ∩ convexHull 𝕜 t ⊆ t :=
  by
  constructor
  · rintro hc t h x ⟨hxs, hxt⟩
    refine hc {x | ↑x ∈ t} ⟨x, hxs⟩ ?_
    rw [Subtype.coe_image_of_subset h]
    exact hxt
  · intro hc t x h
    rw [← Subtype.coe_injective.mem_set_image]
    exact hc (t.image ((↑) : s → E)) (Subtype.coe_image_subset s t) ⟨x.prop, h⟩

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