map_sup — Mathlib

English

Let f be a ring homomorphism and s, t subfields of K. The image of the join equals the join of the images: (s ⊔ t).map f = s.map f ⊔ t.map f.

Русский

Пусть f — кольцеобразный гомоморфизм, и s, t — подполе K. Образ их соединения равен соединению образов: (s ⊔ t).map f = s.map f ⊔ t.map f.

LaTeX

$$$$(s \sqcup t).map f = s.map f \sqcup t.map f$$$$

Lean4

theorem map_sup (s t : Subfield K) (f : K →+* L) : (s ⊔ t).map f = s.map f ⊔ t.map f :=
  (gc_map_comap f).l_sup

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