whiskerLeftIso_refl — Mathlib

English

For any W, X in C, whiskerLeftIso W (Iso.refl X) equals the identity on W ⊗ X.

Русский

Для любых W, X в C обертка слева через тождественный изоморфизм равна тождественному морфизму на W ⊗ X.

LaTeX

$$$ whiskerLeftIso W (Iso.refl X) = Iso.refl (W \\otimes X) $$$

Lean4

@[simp]
theorem whiskerLeftIso_refl (W X : C) : whiskerLeftIso W (Iso.refl X) = Iso.refl (W ⊗ X) :=
  Iso.ext (whiskerLeft_id W X)

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