image_symm_image — Mathlib

English

For f: M1 ≃SL[σ₁₂] M2 and f': M2 ≃SL[σ₂₃] M3, the composition of their coerced linear maps equals the coerced composition: (f' : M2 →SL[σ₂₃] M3) ∘ (f : M1 →SL[σ₁₂] M2) = (f.trans f' : M1 →SL[σ₁₃] M3).

Русский

Для f: M1 ≃SL[σ₁₂] M2 и f': M2 ≃SL[σ₂₃] M3 композиция приведённых линейных отображений равна линейному отображению, соответствующему композиции: (f' ∘ f) = (f.trans f').

LaTeX

$$$ (f' : M_2 \\toSL[\\sigma_{23}] M_3) \\circ (f : M_1 \\toSL[\\sigma_{12}] M_2) = (f \\text{.trans} f' : M_1 \\toSL[\\sigma_{13}] M_3) $$$

Lean4

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

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