symm_image_image — Mathlib

English

For e1: M1 ≃SL[σ₁₂] M2 and e2: M2 ≃SL[σ₂₃] M3 and c ∈ M1, (e2.trans e1).symm c = e2.symm (e1.symm c).

Русский

Для e1: M1 ≃SL[σ₁₂] M2 и e2: M2 ≃SL[σ₂₃] M3 и c ∈ M1, (e2.trans e1).symm c = e2.symm (e1.symm c).

LaTeX

$$$ (e_2 \\trans e_1)^{-1}(c) = e_2^{-1}(e_1^{-1}(c)) $$$

Lean4

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

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