map_sup — Mathlib

English

Let f be a Lie-module hom between Lie submodules. Then the image under f preserves the supremum of two submodules: the image of the join equals the join of the images.

Русский

Пусть f—гомоморфизм модулей Ли между подпространствами Ли. Тогда образ подпространств сохраняет наивысшее (супремум): образ суммы двух подпространств равен сумме их образов.

LaTeX

$$$ (N \sqcup N_2).map f = N.map f \sqcup N_2.map f $$$

Lean4

@[simp]
theorem map_sup : (N ⊔ N₂).map f = N.map f ⊔ N₂.map f :=
  (gc_map_comap f).l_sup

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