iso_w' — Mathlib

English

If e : Arrow.mk f ≅ Arrow.mk g is an isomorphism, then g = e.inv.left ≫ f ≫ e.hom.right.

Русский

Если e : Arrow.mk f ≅ Arrow.mk g является изоморфизмом стрел, то g = e.inv.left ≫ f ≫ e.hom.right.

LaTeX

$$$\forall W,X,Y,Z\; (f: W \to X)\; (g: Y \to Z)\; (e:\, Arrow.mk f \cong Arrow.mk g):\; g = e.inv.left \circ f \circ e.hom.right$$$

Lean4

theorem iso_w' {W X Y Z : T} {f : W ⟶ X} {g : Y ⟶ Z} (e : Arrow.mk f ≅ Arrow.mk g) : g = e.inv.left ≫ f ≫ e.hom.right :=
  iso_w e

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