nonempty_of_mem_faces

Mathlib.Analysis.Convex.SimplicialComplex.Basic

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

English

If a Finset is a member of the faces of a simplicial complex K, then the Finset is nonempty.

Русский

Если финисет принадлежит граням симпликальных комплексов K, то он непуст.

LaTeX

$$$s \in K.faces \Rightarrow s \neq \emptyset$$$

Lean4

theorem nonempty_of_mem_faces (hs : s ∈ K.faces) : s.Nonempty := by rw [Finset.nonempty_iff_ne_empty]; rintro rfl;
  exact K.empty_notMem hs

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

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

Разделы

Аффилиация

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