preimage_symm_preimage

Mathlib.Topology.Algebra.Module.Equiv

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

English

For e: M1 ≃SL[σ₁₂] M2 and x ∈ M2, y ∈ M1, y = e.symm x iff e y = x.

Русский

Для e: M1 ≃SL[σ₁₂] M2 и x ∈ M2, y ∈ M1, y = e.symm x ⇔ e y = x.

LaTeX

$$$ y = e^{-1}(x) \\iff e(y) = x $$$

Lean4

@[simp]
protected theorem preimage_symm_preimage (e : M₁ ≃SL[σ₁₂] M₂) (s : Set M₁) : e ⁻¹' (e.symm ⁻¹' s) = s :=
  e.symm.symm_preimage_preimage s

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

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

Разделы

Аффилиация

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