closure_subset_closedAbsConvexHull

English

If s ⊆ t, AbConvex 𝕜 t, and IsClosed t, then closedAbsConvexHull 𝕜 s ⊆ t.

Русский

Если s ⊆ t, t AbsConvex и t замкнуто, то closedAbsConvexHull 𝕜 s ⊆ t.

LaTeX

$$$$ s \\subseteq t \\Rightarrow \\operatorname{AbsConvex} 𝕜 t \\Rightarrow IsClosed t \\Rightarrow \\operatorname{closedAbsConvexHull}_{𝕜} (s) \\subseteq t. $$$$

Lean4

theorem closure_subset_closedAbsConvexHull {s : Set E} : closure s ⊆ closedAbsConvexHull 𝕜 s :=
  closure_minimal subset_closedAbsConvexHull isClosed_closedAbsConvexHull

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