absConvexHull_subset_closedAbsConvexHull

English

Same as 52205/52206: the minimal closed AbsConvexHull containing s is contained in any closed AbsConvex superset.

Русский

То же: минимальная замкнутая AbsConvexHull, содержащая s, включена в любую замкнутую AbsConvex надмножество.

LaTeX

$$$$ s \\subseteq t \\;\\to\\; AbsConvex 𝕜 t \\;\\to\\; IsClosed t \\Rightarrow closedAbsConvexHull 𝕜 s \\subseteq t. $$$$

Lean4

theorem absConvexHull_subset_closedAbsConvexHull {s : Set E} : (absConvexHull 𝕜) s ⊆ (closedAbsConvexHull 𝕜) s :=
  absConvexHull_min subset_closedAbsConvexHull absConvex_convexClosedHull

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