symm_preimage_preimage — Mathlib

English

The preimage under symm of the preimage under e of a set equals the set: e.symm^{-1}( e^{-1}(S) ) = S.

Русский

Обратное по отношению к симм от обратного по отношению к e множества S есть само S.

LaTeX

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

Lean4

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

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