closedConvexHull_min — Mathlib

English

If s ⊆ t and t is convex and closed, then closedConvexHull 𝕜 s ⊆ t.

Русский

Если s ⊆ t и t выпукло и замкнуто, то closedConvexHull 𝕜 s ⊆ t.

LaTeX

$$s ⊆ t ∧ Convex 𝕜 t ∧ IsClosed t ⇒ closedConvexHull 𝕜 s ⊆ t$$

Lean4

theorem closedConvexHull_min {s t : Set E} (hst : s ⊆ t) (h_conv : Convex 𝕜 t) (h_closed : IsClosed t) :
    closedConvexHull 𝕜 s ⊆ t :=
  (closedConvexHull 𝕜).closure_min hst ⟨h_conv, h_closed⟩

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