isIso_fst_of_isIso — Mathlib

English

If h is a pullback and g is an isomorphism, then fst is an isomorphism.

Русский

Если квадрат является пределом, и g является изоморфизмом, то fst — изоморфизм.

LaTeX

$$$ IsPullback fst snd f g \Rightarrow [IsIso g] \Rightarrow IsIso fst $$$

Lean4

theorem isIso_fst_of_isIso (h : IsPullback fst snd f g) [IsIso g] : IsIso fst :=
  by
  have := h.hasPullback
  rw [← h.isoPullback_hom_fst]
  infer_instance

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