instEquivLike — Mathlib

English

The type of continuous affine equivalences carries a canonical EquivLike structure, i.e., one can view elements as functions with an inverse and coherent composition.

Русский

У типа непрерывных аффинных эквивалентов имеется каноническая структура EquivLike: можно рассматривать элементы как функции с обратной и совместимостью композиции.

LaTeX

$$$\\text{EquivLike}((P_1 \\simeq_A^k P_2), P_1, P_2)$$$

Lean4

instance instEquivLike : EquivLike (P₁ ≃ᴬ[k] P₂) P₁ P₂
    where
  coe f := f.toFun
  inv f := f.invFun
  left_inv f := f.left_inv
  right_inv f := f.right_inv
  coe_injective' _ _ h _ := toAffineEquiv_injective (DFunLike.coe_injective h)

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