closedAbsConvexHull_min — Mathlib

English

Same as 52205: s ⊆ t, AbsConvex t, IsClosed t implies closedAbsConvexHull s ⊆ t.

Русский

То же самое: s ⊆ t, AbsConvex t, IsClosed t ⇒ closedAbsConvexHull 𝕜 s ⊆ t.

LaTeX

$$$$ s \\subseteq t \\rightarrow AbsConvex 𝕜 t \\rightarrow IsClosed t \\rightarrow closedAbsConvexHull 𝕜 s \\subseteq t. $$$$

Lean4

theorem closedAbsConvexHull_min {s t : Set E} (hst : s ⊆ t) (h_conv : AbsConvex 𝕜 t) (h_closed : IsClosed t) :
    closedAbsConvexHull 𝕜 s ⊆ t :=
  (closedAbsConvexHull 𝕜).closure_min hst ⟨h_conv, h_closed⟩

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