map_iSup — Mathlib

English

Let f be a surjective semilinear map. For any family of submodules p_i, the image of the supremum is the supremum of the images: map f (⨆ i, p_i) = ⨆ i, map f (p_i).

Русский

Пусть f — сюръективное линейно-отображение. Для любой семейства подмодулей p_i выполняется: image_f(⋁_i p_i) = ⋁_i image_f(p_i).

LaTeX

$$$\operatorname{map} f \left( \bigvee_{i} p_i \right) = \bigvee_{i} \operatorname{map} f (p_i)$$$

Lean4

@[simp]
theorem map_iSup {ι : Sort*} (f : F) (p : ι → Submodule R M) : map f (⨆ i, p i) = ⨆ i, map f (p i) :=
  (gc_map_comap f : GaloisConnection (map f) (comap f)).l_iSup

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