pushout_inl_iso_of_right_iso — Mathlib

English

Let f: X → Y and g: X → Z with g an isomorphism. Then the pushout.inr f g is an isomorphism.

Русский

Пусть f: X → Y и g: X → Z с g изоморфизм. Тогда pushout.inr f g является изоморфизмом.

LaTeX

$$$\text{IsIso}(\text{pushout.inr}(f,g)).$$$

Lean4

instance pushout_inl_iso_of_right_iso : IsIso (pushout.inl _ _ : _ ⟶ pushout f g) :=
  by
  refine ⟨⟨pushout.desc (𝟙 _) (inv g ≫ f) (by simp), by simp, ?_⟩⟩
  ext
  · simp
  · simp [pushout.condition]

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