map_zero_one'

Mathlib.CategoryTheory.ComposableArrows

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ComposableArrows.Precomp.map_zero_one'

English

A convenience version: map F f 0 ⟨0+1, ...⟩ equals f.

Русский

Удобный вариант: map F f 0 ⟨0+1, ...⟩ равно f.

LaTeX

$$$\text{map_zero_one'}: map F f 0 ⟨0+1, \cdots\rangle = f$$$

Lean4

@[simp]
theorem map_zero_one' : map F f 0 ⟨0 + 1, by simp⟩ (by simp) = f :=
  rfl

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

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

Разделы

Аффилиация

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