toN_eq_iff

Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

URI: https://scilib.ai/kg/mathlib#SSet.S.toN_eq_iff

Lean4

theorem toN_eq_iff {x : X.S} {y : X.N} : x.toN = y ↔ y.subcomplex = x.subcomplex :=
  ⟨by rintro rfl; simp, fun h ↦ x.existsUnique_n.unique (by simp) h⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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