toEquiv_mk — Mathlib

English

The Lie module equivalence constructed from data (f, g, h1, h2) has underlying equivalence equal to the usual Equiv.mk with the same components.

Русский

Эквивалентность Ли-модуля, построенная из данных (f, g, h1, h2), имеет свою естественную эквивалентность, равную обычному Equiv.mk с теми же компонентами.

LaTeX

$$$\\operatorname{toEquiv}(\\operatorname{mk}(f,g,h_1,h_2)) = \\operatorname{Equiv.mk}(f,g,h_1,h_2)$$$

Lean4

@[simp]
theorem toEquiv_mk (f : M →ₗ⁅R,L⁆ N) (g : N → M) (h₁ h₂) : toEquiv (mk f g h₁ h₂ : M ≃ₗ⁅R,L⁆ N) = Equiv.mk f g h₁ h₂ :=
  rfl

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