triangle — Mathlib

English

There is an instance that whiskering with a left isomorphism is an isomorphism for CatCospanTransform.

Русский

Существует инстанс, что взвешивание слева вдоль изоморфизма является изоморфизмом в CatCospanTransform.

LaTeX

$$$\\text{IsIso}(\\text{whiskerLeft}(ψ, θ))$$$

Lean4

@[reassoc]
theorem triangle : (α_ ψ (.id _ _) φ).hom ≫ ψ ◁ (λ_ φ).hom = (ρ_ ψ).hom ▷ φ := by cat_disch

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