map_sup — Mathlib

English

Under a ring homomorphism f, the image of the join equals the join of images: map f (s ⊔ t) = map f s ⊔ map f t.

Русский

Пусть f — гомоморфизм колец; образ суммы равен сумме образов: map f (s ⊔ t) = map f s ⊔ map f t.

LaTeX

$$$\\operatorname{map}_f(s \\sqcup t) = \\operatorname{map}_f(s) \\sqcup \\operatorname{map}_f(t)$$$

Lean4

theorem map_sup (s t : NonUnitalSubsemiring R) (f : F) : (map f (s ⊔ t) : NonUnitalSubsemiring S) = map f s ⊔ map f t :=
  @GaloisConnection.l_sup _ _ s t _ _ _ _ (gc_map_comap f)

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