map_sup — Mathlib

English

For subrings s,t of R and a ring hom f, the image of the supremum equals the supremum of the images: map f (s ⊔ t) = map f s ⊔ map f t.

Русский

Образ верхней грань подкольц через отображение равен верхней грани образов: map f (s ⊔ t) = map f s ⊔ map f t.

LaTeX

$$$\\mathrm{map}\,f\\bigl(s \\sqcup t\\bigr) = \\mathrm{map}\,f(s) \\sqcup \\mathrm{map}\,f(t)$$$

Lean4

theorem map_sup (s t : Subring R) (f : R →+* S) : (s ⊔ t).map f = s.map f ⊔ t.map f :=
  (gc_map_comap f).l_sup

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