apply_symm_apply

Mathlib.Topology.Algebra.Module.Equiv

URI: https://scilib.ai/kg/mathlib#ContinuousLinearEquiv.apply_symm_apply

English

For any c ∈ M2, e(e.symm c) = c, showing that e and its inverse undo each other.

Русский

Для любого c ∈ M2 верно e(e.symm c) = c, то есть e и его обратное взаимодействуют как взаимные обратные.

LaTeX

$$$ e(e^{-1}(c)) = c $$$

Lean4

@[simp]
theorem apply_symm_apply (e : M₁ ≃SL[σ₁₂] M₂) (c : M₂) : e (e.symm c) = c :=
  e.1.right_inv c

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru