instEquivLike — Mathlib

English

The type Equiv α β carries a canonical EquivLike structure, making Equiv α β behave as a bijection between α and β.

Русский

Тип Equiv α β содержит каноническую структуру EquivLike, превращающую Equiv α β в биекция между α и β.

LaTeX

$$$\\text{Equiv}(\\alpha,\\beta)\\text{ is equipped with an }\\operatorname{EquivLike} \\text{ structure}. $$$

Lean4

instance : EquivLike (α ≃ β) α β where
  coe := Equiv.toFun
  inv := Equiv.invFun
  left_inv := Equiv.left_inv
  right_inv := Equiv.right_inv
  coe_injective' e₁ e₂ h₁ h₂ := by cases e₁; cases e₂; congr

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