map_eq_mapOfHomotopy — Mathlib

English

Equality of two ways to form a map between mapping cones: the usual map equals the map formed from a homotopy.

Русский

Согласованность двух конструкторов отображения между отображающими конусами: обычное отображение равно отображению, построенному через гомотопию.

LaTeX

$$$map φ_1 φ_2 a b comm = mapOfHomotopy (Homotopy.ofEq comm)$$$

Lean4

theorem map_eq_mapOfHomotopy : map φ₁ φ₂ a b comm = mapOfHomotopy (Homotopy.ofEq comm) := by simp [map, mapOfHomotopy]

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