degenerate_zero

Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

URI: https://scilib.ai/kg/mathlib#SSet.degenerate_zero

English

There are no degenerate 0-simplices.

Русский

Нет degenerate 0-симплексoв.

LaTeX

$$$ X.degenerate(0) = \emptyset $$$

Lean4

@[simp]
theorem degenerate_zero : X.degenerate 0 = ∅ := by
  ext x
  simp only [Set.mem_empty_iff_false, iff_false]
  rintro ⟨m, hm, _⟩
  simp at hm

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

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

Разделы

Аффилиация

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