postcomp — Mathlib

English

If P respects iso, then postcomposition with an isomorphism preserves P.

Русский

Если P сохраняет изоморфизм, то посткомпозиция с изоморфизмом сохраняет P.

LaTeX

$$$P(f) \Rightarrow P(f \;\circ\; e)$ for iso e$$

Lean4

theorem postcomp (P : MorphismProperty C) [P.RespectsIso] {X Y Z : C} (e : Y ⟶ Z) [IsIso e] (f : X ⟶ Y) (hf : P f) :
    P (f ≫ e) :=
  RespectsRight.postcomp (Q := isomorphisms C) e ‹IsIso e› f hf

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