comapEq_symm — Mathlib

English

For a category C, and functions f,g: β → γ with h: f = g, the comapEq operation respects symmetry: comapEq C h.symm = (comapEq C h).symm.

Русский

Для категории C и отображений f,g: β → γ, если h: f = g, то comapEq C h.symm равен симметрии (comapEq C h).symm.

LaTeX

$$$ comapEq\, C\, h^{\\mathrm{symm}} = (comapEq\, C\, h)^{\\mathrm{symm}} $$$

Lean4

theorem comapEq_symm {β γ : Type w} {f g : β → γ} (h : f = g) : comapEq C h.symm = (comapEq C h).symm := by cat_disch

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