toPlus_comp_plusCompIso_inv — Mathlib

English

The plus object construction is compatible with composition with F, respecting the plus constructions for P and P ⋅ F.

Русский

Конструкция plusObj совместима с композициями и с plus-конструкциями для P и P ⋅ F.

LaTeX

$$$(J.plusObj P) ⋙ F \simeq J.plusObj (P ⋙ F)$$$

Lean4

@[simp]
theorem toPlus_comp_plusCompIso_inv : J.toPlus _ ≫ (J.plusCompIso F P).inv = whiskerRight (J.toPlus _) _ := by
  simp [Iso.comp_inv_eq]

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