image_convexHull — Mathlib

English

The convex hull of s is nonempty if and only if s is nonempty.

Русский

Выпуклая оболочка множества непусто тогда и только тогда, когда множество непусто.

LaTeX

$$$ (convexHull 𝕜 s).Nonempty \\iff s.Nonempty $$$

Lean4

theorem image_convexHull {f : E → F} (hf : IsLinearMap 𝕜 f) (s : Set E) : f '' convexHull 𝕜 s = convexHull 𝕜 (f '' s) :=
  Set.Subset.antisymm
    (image_subset_iff.2 <|
      convexHull_min (image_subset_iff.1 <| subset_convexHull 𝕜 _) ((convex_convexHull 𝕜 _).is_linear_preimage hf))
    (convexHull_min (image_mono (subset_convexHull 𝕜 s)) <| (convex_convexHull 𝕜 s).is_linear_image hf)

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