eq_symm_apply

Mathlib.Topology.Algebra.Module.Equiv

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

English

For e: M1 ≃SL[σ₁₂] M2 and x ∈ M2, e.symm x is the unique element whose forward image is x.

Русский

Для e: M1 ≃SL[σ₁₂] M2 и x ∈ M2, e.symm x — это уникальный элемент, чьё прямое изображение равно x.

LaTeX

$$$ e.symm x = y \\Longrightarrow e(y) = x$$$

Lean4

theorem eq_symm_apply (e : M₁ ≃SL[σ₁₂] M₂) {x y} : y = e.symm x ↔ e y = x :=
  e.toLinearEquiv.eq_symm_apply

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

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

Разделы

Аффилиация

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