map_sup — Mathlib

English

The map operation preserves the supremum of subsemigroups: (S ⊔ T).map f = S.map f ⊔ T.map f.

Русский

Операция отображения сохраняет верхнюю грань объединения подполугрупп: (S ⊔ T).map f = S.map f ⊔ T.map f.

LaTeX

$$$(S \sqcup T).map f = S.map f \sqcup T.map f$$

Lean4

@[to_additive]
theorem map_sup (S T : Subsemigroup M) (f : M →ₙ* N) : (S ⊔ T).map f = S.map f ⊔ T.map f :=
  (gc_map_comap f).l_sup

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