instTrans — Mathlib

English

There is a canonical composition operation on equivalences, making the collection of all equivalences closed under composition.

Русский

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

LaTeX

$$$\forall e_1:\alpha \simeq \beta,\forall e_2:\beta \simeq \gamma,\ e_1 \circ e_2 \text{ (или } e_2 \circ e_1\text{)} \text{ является } \alpha \simeq \gamma$$$

Lean4

@[simps]
instance : Trans Equiv Equiv Equiv where trans := Equiv.trans

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