image_convexHull — Mathlib

English

The convex hull of s equals zero if and only if s equals zero.

Русский

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

LaTeX

$$$ convexHull 𝕜 s = 0 \\iff s = 0 $$$

Lean4

theorem image_convexHull (f : E →ᵃ[𝕜] F) (s : Set E) : f '' convexHull 𝕜 s = convexHull 𝕜 (f '' s) :=
  by
  apply Set.Subset.antisymm
  · rw [Set.image_subset_iff]
    refine convexHull_min ?_ ((convex_convexHull 𝕜 (f '' s)).affine_preimage f)
    rw [← Set.image_subset_iff]
    exact subset_convexHull 𝕜 (f '' s)
  · exact convexHull_min (Set.image_mono (subset_convexHull 𝕜 s)) ((convex_convexHull 𝕜 s).affine_image f)

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