instIsIsoHomFromCommaOfIsIso — Mathlib

English

If i is an isomorphism in a comma, then homFromCommaOfIsIso i is an isomorphism, and its inverse is homFromCommaOfIsIso i⁻¹.

Русский

Если i — изоморфизм в комме, то homFromCommaOfIsIso i является изоморфизмом, и его обратный гомоморфизм равен homFromCommaOfIsIso i⁻¹.

LaTeX

$$$\\text{IsIso}(\\mathrm{homFromCommaOfIsIso}(i))$$$

Lean4

instance [Q.RespectsIso] [W.RespectsIso] {X Y : P.Comma L R Q W} (i : X.toComma ⟶ Y.toComma) [IsIso i] :
    IsIso (homFromCommaOfIsIso i) := by
  constructor
  use homFromCommaOfIsIso (inv i)
  constructor <;> ext : 1 <;> simp

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