whiskerRight_congr — Mathlib

English

If g=g' then whiskerRight η g = eqToHom(h) ≫ whiskerRight η g' ≫ eqToHom(h) for suitable η and h.

Русский

Если g = g', то whiskerRight η g = eqToHom(h) ≫ whiskerRight η g' ≫ eqToHom(h) при подходящих η и h.

LaTeX

$$$\\eta \\ ▷ g = eqToHom(\\cdot) \\gg \\eta \\▷ g' \\gg eqToHom(\\cdot)$$$

Lean4

theorem whiskerRight_congr {y z : B} {g g' : y ⟶ z} (h : g = g') {x : B} {f f' : x ⟶ y} (η : f ⟶ f') :
    η ▷ g = eqToHom (by rw [h]) ≫ η ▷ g' ≫ eqToHom (by rw [h]) :=
  by
  subst h
  simp

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