trW_of_isIso — Mathlib

English

If f : X → Y is an isomorphism, then P.trW f holds (assuming P.ContainsZero).

Русский

Если f : X → Y является изоморфизмом, то P.trW f, при условии P.ContainsZero.

LaTeX

$$$P.ContainsZero \\Rightarrow \\forall X Y, \\forall f: X \\to Y, [\\text{IsIso } f] \\Rightarrow P.trW f$$$

Lean4

theorem trW_of_isIso [P.ContainsZero] {X Y : C} (f : X ⟶ Y) [IsIso f] : P.trW f :=
  by
  refine (P.trW.arrow_mk_iso_iff ?_).1 (MorphismProperty.id_mem _ X)
  exact Arrow.isoMk (Iso.refl _) (asIso f)

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