unit_uniqueUpToIso_inv — Mathlib

English

As in the previous item, the inverse relation also holds up to the inverse iso, ensuring a unique unit up to isomorphism both directions.

Русский

Как и в предыдущем пункте, обратная связь сохраняется через обратный изоморфизм, обеспечивая единство единицы вплоть до изоморфизма в обе стороны.

LaTeX

$$$ h'.unit \\;\\circ\\; (\\text{uniqueUpToIso } h h').inv = h.unit $$$

Lean4

@[reassoc (attr := simp)]
theorem unit_uniqueUpToIso_inv (h : DayConvolution F G) (h' : DayConvolution F G) :
    h'.unit ≫ Functor.whiskerLeft (tensor C) (h.uniqueUpToIso h').inv = h.unit := by simp [uniqueUpToIso]

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