map_sup — Mathlib

English

Mapping preserves suprema: the image of S ⊔ T equals the supremum of the images.

Русский

Образ отображения сохраняет верхние пределы: образ S ⊔ T равен образу S ⊔ образу T.

LaTeX

$$$ (f : F)\\, (S,T) : \\mathrm{NonUnitalSubalgebra}\\, R\\, A \\to \\mathrm{NonUnitalSubalgebra}\\, R\\, B,\\; (S \\sqcup T).map f = S.map f \\sqcup T.map f $$$

Lean4

theorem map_sup [IsScalarTower R B B] [SMulCommClass R B B] (f : F) (S T : NonUnitalSubalgebra R A) :
    ((S ⊔ T).map f : NonUnitalSubalgebra R B) = S.map f ⊔ T.map f :=
  (NonUnitalSubalgebra.gc_map_comap f).l_sup

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