genWeightSpace_genWeightSpaceOf_map_incl

English

For a weight space inclusion map, the mapped weight space coincides with the target weight space via the inclusion.

Русский

При отображении включения весового пространства карта отображает обе стороны совпадающими образами.

LaTeX

$$$(\operatorname{genWeightSpace}(M,χ))\map (\mathrm{incl}) = \operatorname{genWeightSpace}(N,χ)$$$

Lean4

theorem genWeightSpace_genWeightSpaceOf_map_incl (x : L) (χ : L → R) :
    (genWeightSpace (genWeightSpaceOf M (χ x) x) χ).map (genWeightSpaceOf M (χ x) x).incl = genWeightSpace M χ := by
  simpa [map_genWeightSpace_eq_of_injective (genWeightSpaceOf M (χ x) x).injective_incl] using
    genWeightSpace_le_genWeightSpaceOf M x χ

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