map — Mathlib

English

Let f be a continuous linear map from M to N and s a closed submodule of M. Then the closure of the image f(s) is a closed submodule of N.

Русский

Пусть f: M →L[R] N — непрерывно линейное отображение, и s — замкнутый подмодуль M. Тогда замыкание образа f(s) является замкнутым подмодулем N.

LaTeX

$$$ClosedSubmodule.map(f,s) = (s.toSubmodule.map f).closure$$$

Lean4

/-- The closure of the image of a closed submodule under a continuous linear map is a closed
submodule.

`ClosedSubmodule.map f` is left-adjoint to `ClosedSubmodule.comap f`.
See `ClosedSubmodule.gc_map_comap`. -/
def map (f : M →L[R] N) (s : ClosedSubmodule R M) : ClosedSubmodule R N :=
  (s.toSubmodule.map f).closure

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