map_sup — Mathlib

English

The map operation distributes over sup (join): map f of the join S ⊔ T equals the join of map f S and map f T.

Русский

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

LaTeX

$$$\mathrm{map}\!\_f\,(S \sqcup T) = \mathrm{map}\!\_f\,S \sqcup \mathrm{map}\!\_f\,T$$$

Lean4

@[to_additive]
theorem map_sup (S T : Submonoid M) (f : F) : (S ⊔ T).map f = S.map f ⊔ T.map f :=
  (gc_map_comap f : GaloisConnection (map f) (comap f)).l_sup

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