convexJoin_subset_convexHull

Mathlib.Analysis.Convex.Join

URI: https://scilib.ai/kg/mathlib#convexJoin_subset_convexHull

← MathLib Explorer

English

convexJoin 𝕜 s t ⊆ convexHull 𝕜 (s ∪ t).

Русский

convexJoin 𝕜 s t ⊆ convexHull 𝕜 (s ∪ t).

LaTeX

$$$ convexJoin 𝕜 s t \subseteq convexHull 𝕜 (s \cup t) $$$

Lean4

theorem convexJoin_subset_convexHull (s t : Set E) : convexJoin 𝕜 s t ⊆ convexHull 𝕜 (s ∪ t) :=
  convexJoin_subset (subset_union_left.trans <| subset_convexHull _ _)
      (subset_union_right.trans <| subset_convexHull _ _) <|
    convex_convexHull _ _

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru