map_sup — Mathlib

English

The image under map distributes over the supremum of a family of ideals: map f (I ⊔ J) = map f I ⊔ map f J.

Русский

Образ под отображением распределяется по наибольшему элементу семейства идеалов: map f (I ⊔ J) = map f I ⊔ map f J.

LaTeX

$$$\\operatorname{map} f(I \\sqcup J) = \\operatorname{map} f I \\sqcup \\operatorname{map} f J$$$

Lean4

theorem map_sup : (I ⊔ J).map f = I.map f ⊔ J.map f :=
  (gc_map_comap f : GaloisConnection (map f) (comap f)).l_sup

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