map_genWeightSpace_eq — Mathlib

English

If f is injective, then the map of genWeightSpace M χ along f equals genWeightSpace M2 χ ∩ range.

Русский

Если f инъективен, отображение genWeightSpace(M, χ) по f равняется genWeightSpace(M2, χ) ∩ range.

LaTeX

$$$\operatorname{map} f (\operatorname{genWeightSpace}(M,χ)) = \operatorname{genWeightSpace}(M2,χ) \cap \operatorname{range}(f)$$$

Lean4

theorem map_genWeightSpace_eq (e : M ≃ₗ⁅R,L⁆ M₂) : (genWeightSpace M χ).map e = genWeightSpace M₂ χ := by
  simp [map_genWeightSpace_eq_of_injective e.injective]

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