instMonoδ

Mathlib.AlgebraicTopology.SimplexCategory.Basic

URI: https://scilib.ai/kg/mathlib#SimplexCategory.instMonoδ

English

For every n and i in Fin(n+2), δ_i is a mono morphism.

Русский

Для каждого n и i в Fin(n+2) δ_i моно.

LaTeX

$$$\\\\forall n \\\\forall i \\\\in \\\\mathrm{Fin}(n+2),\\\\operatorname{Mono}(\\\\delta_i)$$$

Lean4

instance {n : ℕ} {i : Fin (n + 2)} : Mono (δ i) :=
  by
  rw [mono_iff_injective]
  exact Fin.succAbove_right_injective

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

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

Разделы

Аффилиация

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