facets_subset

Mathlib.Analysis.Convex.SimplicialComplex.Basic

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

English

The collection of facets is a subset of all faces.

Русский

Множество фасет является подмножеством множества граней.

LaTeX

$$K.facets \\subseteq K.faces$$

Lean4

theorem facets_subset : K.facets ⊆ K.faces := fun _ hs => hs.1

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

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

Разделы

Аффилиация

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