map_sup — Mathlib

English

Let f be a surjective semilinear map between modules. For any submodules p and p' of the domain, the image of their sum equals the sum of their images: f(p + p') = f(p) + f(p').

Русский

Пусть f — сюръективное полинейное отображение между модулями. Тогда для любых подмодуля p и p' имеем: f(p + p') = f(p) + f(p').

LaTeX

$$$\operatorname{map} f (p \sqcup p') = \operatorname{map} f p \sqcup \operatorname{map} f p'$$$

Lean4

@[simp]
theorem map_sup (f : F) : map f (p ⊔ p') = map f p ⊔ map f p' :=
  (gc_map_comap f : GaloisConnection (map f) (comap f)).l_sup

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