whisker_eq — Mathlib

English

Let f: X → Y and g, h: Y → Z be morphisms. If g = h, then f ≫ g = f ≫ h.

Русский

Пусть f: X → Y и g, h: Y → Z — морфизмы. Если g = h, то f ∘ g = f ∘ h.

LaTeX

$$$ \\forall X,Y,Z\\, \\forall f:X\\to Y\\, \\forall g,h:Y\\to Z,\\ g = h \\Rightarrow g \\circ f = h \\circ f $$$

Lean4

/-- precompose an equation between morphisms by another morphism -/
theorem whisker_eq (f : X ⟶ Y) {g h : Y ⟶ Z} (w : g = h) : f ≫ g = f ≫ h := by rw [w]

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