homOfEq_trans — Mathlib

English

The transport map f ↦ homOfEq f hX hY is injective: if two transported arrows are equal, then the original arrows are equal.

Русский

Отображение переноса стрел инъективно: если два перенесённых стрел равны, то исходные стрелы равны.

LaTeX

$$$\\operatorname{homOfEq}(f,h_X,h_Y) = \\operatorname{homOfEq}(g,h_X,h_Y) \\Rightarrow f = g$$$

Lean4

@[simp]
theorem homOfEq_trans {X Y : V} (f : X ⟶ Y) {X' Y' : V} (hX : X = X') (hY : Y = Y') {X'' Y'' : V} (hX' : X' = X'')
    (hY' : Y' = Y'') : homOfEq (homOfEq f hX hY) hX' hY' = homOfEq f (hX.trans hX') (hY.trans hY') :=
  by
  subst hX hY hX' hY'
  rfl

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