mem_degenerate_iff_notMem_nonDegenerate

Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

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

English

An n-simplex lies in the degenerate set exactly when it is not in the non-degenerate set.

Русский

i-симплекс лежит в degenerate тогда, когда он не в nonDegenerate.

LaTeX

$$$ x \in X_{\text{degenerate}}(n) \;\iff\; x \notin X_{\text{nonDegenerate}}(n) $$$

Lean4

theorem mem_degenerate_iff_notMem_nonDegenerate (x : X _⦋n⦌) : x ∈ X.degenerate n ↔ x ∉ X.nonDegenerate n := by
  simp [nonDegenerate]

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

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

Разделы

Аффилиация

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