instEquivLike — Mathlib

English

The collection of LieModuleEquiv objects forms an EquivLike structure, i.e., they behave like equivalences with associated inverse maps.

Русский

Множество объектов LieModuleEquiv образуют структуру EquivLike, т.е. ведут себя как эквивелентности с обратными отображениями.

LaTeX

$$$\text{LieModuleEquiv}(R,L,M,N) \to\text{Equiv}(M,N)$$$

Lean4

instance : EquivLike (M ≃ₗ⁅R,L⁆ N) M N where
  coe f := f.toFun
  inv f := f.invFun
  left_inv f := f.left_inv
  right_inv f := f.right_inv
  coe_injective' f g h₁ h₂ := by cases f; cases g; simp at h₁ h₂; simp [*]

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