vertices_subset_space

Mathlib.Analysis.Convex.SimplicialComplex.Basic

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

English

The vertex set is contained in the space of the complex.

Русский

Множество вершин содержится в пространстве комплекса.

LaTeX

$$K.vertices \\subseteq K.space$$

Lean4

theorem vertices_subset_space : K.vertices ⊆ K.space :=
  vertices_eq.subset.trans <| iUnion₂_mono fun x _ => subset_convexHull 𝕜 (x : Set E)

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

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

Разделы

Аффилиация

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