pullback_inv_snd_fst_of_left_isIso

English

If f is an isomorphism, then inv(snd) ; fst = g ; inv(f).

Русский

Если f — изоморфизм, то inv(snd) ; fst = g ; inv(f).

LaTeX

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

Lean4

@[reassoc (attr := simp)]
theorem pullback_inv_snd_fst_of_left_isIso : inv (pullback.snd f g) ≫ pullback.fst f g = g ≫ inv f := by
  rw [IsIso.inv_comp_eq, ← pullback.condition_assoc, IsIso.hom_inv_id, Category.comp_id]

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