pullbackSymmetry_inv_comp_snd — Mathlib

English

The inverse of the symmetry, composed with the snd projection, equals the fst projection on swapped legs.

Русский

Обратный симметрии, компонуемый с snd, равен fst после перестановки ног.

LaTeX

$$$$ (\mathrm{pullbackSymmetry}(f,g)).\mathrm{inv} \circ \mathrm{pullback}.\mathrm{snd}(f,g) = \mathrm{pullback}.\mathrm{fst}(g,f). $$$$

Lean4

@[reassoc (attr := simp)]
theorem pullbackSymmetry_inv_comp_snd [HasPullback f g] :
    (pullbackSymmetry f g).inv ≫ pullback.snd f g = pullback.fst g f := by simp [Iso.inv_comp_eq]

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