map_sup — Mathlib

English

The image of the sum of two subalgebras under a star algebra homomorphism equals the sum of the images.

Русский

Образ суммы двух подпалебр под гомоморфизмом сохраняется по сумме образов.

LaTeX

$$$\operatorname{map} f (S \sqcup T) = \operatorname{map} f S \sqcup \operatorname{map} f T$$$

Lean4

theorem map_sup (f : A →⋆ₐ[R] B) (S T : StarSubalgebra R A) : map f (S ⊔ T) = map f S ⊔ map f T :=
  (StarSubalgebra.gc_map_comap f).l_sup

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