inl_comp_pushoutSymmetry_inv — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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