inverseAssociatorIsEquivalence — Mathlib

English

The inverse associator is an equivalence; it is the inverse of the associator up to equivalence.

Русский

Обратный ассоциатор является эквивалентностью; он является обратной к ассоциатору в эквивалентном смысле.

LaTeX

$$$\text{inverseAssociator} \text{ IsEquivalence}$$$

Lean4

instance inverseAssociatorIsEquivalence : (inverseAssociator C D E).IsEquivalence :=
  (by infer_instance : (associativity C D E).inverse.IsEquivalence)
    -- TODO pentagon natural transformation? ...satisfying?

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