cancel_left_of_respectsIso — Mathlib

English

If P is a RespectsIso property, then P(f ≫ g) is equivalent to P g when f is an isomorphism.

Русский

Если P обладает свойством RespectsIso, то P(f ≫ g) эквивалентно P(g) когда f — изоморфизм.

LaTeX

$$$P(f \!\gg g) \iff P(g)$ при $f$ изоморфизм$$

Lean4

theorem cancel_left_of_respectsIso (P : MorphismProperty C) [hP : RespectsIso P] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
    [IsIso f] : P (f ≫ g) ↔ P g :=
  ⟨fun h => by simpa using RespectsIso.precomp P (inv f) (f ≫ g) h, RespectsIso.precomp P f g⟩

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