range — Mathlib

English

The range of a Lie-module morphism is a Lie-submodule of the target.

Русский

Образ гомоморфизма Ли-модулей является подмодулем Ли в целевом модуле.

LaTeX

$$$ \operatorname{range}(f) = (\operatorname{map} f \; \top).copy (\operatorname{Set.range} f) (Set.image_univ.none) $$$

Lean4

/-- The range of a morphism of Lie modules `f : M → N` is a Lie submodule of `N`.
See Note [range copy pattern]. -/
def range : LieSubmodule R L N :=
  (LieSubmodule.map f ⊤).copy (Set.range f) Set.image_univ.symm

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