convexHull_subset_space

Mathlib.Analysis.Convex.SimplicialComplex.Basic

URI: https://scilib.ai/kg/mathlib#Geometry.SimplicialComplex.convexHull_subset_space

English

If s is a face of K, then the convex hull of s is contained in the space of K.

Русский

Если s является гранью K, то выпуклая оболочка s содержится внутри пространства K.

LaTeX

$$$(s \\in K.faces) \\Rightarrow convexHull 𝕜 ↑s \\subseteq K.space$$$

Lean4

theorem convexHull_subset_space (hs : s ∈ K.faces) : convexHull 𝕜 ↑s ⊆ K.space :=
  by
  convert subset_biUnion_of_mem hs
  rfl

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

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

Разделы

Аффилиация

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