image_eq_preimage

Mathlib.Topology.Algebra.Module.Equiv

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

English

The symm of a symm is the original: e.symm.symm = e.

Русский

Обратное от обратного равно самому e.

LaTeX

$$$ e^{\\smash{\\text{symm}}} = e $$$

Lean4

protected theorem image_eq_preimage (e : M₁ ≃SL[σ₁₂] M₂) (s : Set M₁) : e '' s = e.symm ⁻¹' s :=
  e.toLinearEquiv.toEquiv.image_eq_preimage s

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

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

Разделы

Аффилиация

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