app_one

Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

URI: https://scilib.ai/kg/mathlib#CategoryTheory.toNerve₂.mk.app_one

English

On 1-simplices, mk.app sends a 1-simplex f to the corresponding mk₁ of its image under F.

Русский

На 1-симплексах mk.app отправляет 1-симплекс f в соответствующий mk₁ изображения под F.

LaTeX

$$$\mathrm{mk.app}\;F\;⟦1⟧\;f = \mathrm{mk}_1\big( F(f) \big)$$$

Lean4

@[simp]
theorem app_one (f : X _⦋1⦌₂) : mk.app F (⦋1⦌₂) f = .mk₁ (F.map ⟨f, rfl, rfl⟩) :=
  rfl

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

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

Разделы

Аффилиация

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