inr_comp_pushoutSymmetry_inv — Mathlib

English

The right injection composed with the inverse of the symmetry equals the left injection for the pushout of swapped legs.

Русский

Правый инъекция, композиция с обратной симметрии равна левому инъекции при пушауте после перестановки ног.

LaTeX

$$$$ \mathrm{pushout.inr}(g,f) \circ (\mathrm{pushoutSymmetry}(f,g))^{-1} = \mathrm{pushout.inl}(f,g). $$$$

Lean4

@[reassoc (attr := simp)]
theorem inr_comp_pushoutSymmetry_inv [HasPushout f g] : pushout.inr _ _ ≫ (pushoutSymmetry f g).inv = pushout.inl _ _ :=
  by simp [Iso.comp_inv_eq]

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