isIso_inr_of_isIso — Mathlib

English

If h is a pushout of f,g and f is epi, then the left leg inl is an isomorphism.

Русский

Если f эпиморфизм и h — пушаут f g, то левая ножка inl является изоморфизмом.

LaTeX

$$$IsPushout\ f\ g\ inl\ inr \rightarrow [IsIso f] \Rightarrow IsIso inl$$$

Lean4

theorem isIso_inr_of_isIso (h : IsPushout f g inl inr) [IsIso f] : IsIso inr :=
  by
  have := h.hasPushout
  rw [← h.inr_isoPushout_inv]
  infer_instance

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