eq_whisker — Mathlib

English

If two morphisms f and g are equal, then post-composition with any morphism h preserves equality: f ≡ g implies f ∘ h ≡ g ∘ h.

Русский

Если два морфизма f и g равны, то послекомпоновка слева от них любым морфизмом h сохраняет равенство: f = g ⇒ f ∘ h = g ∘ h.

LaTeX

$$$f = g \\;\\Rightarrow\\; f \\circ h = g \\circ h$$$

Lean4

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

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