map_sup — Mathlib

English

A RingHom preserves joins of subsemirings: the image of the join equals the join of the images.

Русский

Гомоморф сохраняет объединение (сумму) двух подполей: образ объединения равен объединению образов.

LaTeX

$$$\operatorname{Subsemiring.map}\ f\,(s \sqcup t) = \operatorname{Subsemiring.map}\ f\ s \sqcup \operatorname{Subsemiring.map}\ f\ t$$$

Lean4

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

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