whiskerRight_isIso — Mathlib

English

If η is an isomorphism in a hom-category between g and h, then whiskering on the left by f yields an isomorphism f ◁ η.

Русский

Если η – изоморфизм в гом-категории между g и h, то левое взвешивание f ◁ η дает изоморфизм.

LaTeX

$$$ \text{IsIso}(f \triangleleft η) \;\text{given } [IsIso η] $$$

Lean4

instance whiskerRight_isIso {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c) [IsIso η] : IsIso (η ▷ h) :=
  (whiskerRightIso (asIso η) h).isIso_hom

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