spineInjective

Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

URI: https://scilib.ai/kg/mathlib#SSet.StrictSegal.spineInjective

English

The spineEquiv map is injective for all m,h, equivalently, the associated function is injective.

Русский

Отображение spineEquiv инъективно для всех m,h; соответствующая функция инъективна.

LaTeX

$$spineEquiv m h : X_{⟨m⟩} -> Path(X,m) is injective$$

Lean4

theorem spineInjective : Function.Injective (sx.spineEquiv n) :=
  Equiv.injective _

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

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

Разделы

Аффилиация

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