map_iSup — Mathlib

English

Taking a sup over a family of submonoids and then mapping yields the same as mapping each and then taking the sup: (iSup s).map f = ⨆ i, (s i).map f.

Русский

Семейство подмономиодов сопряжено с объединением: map f от iSup s равно верхнему пределу по i: ⨆ i, (s i).map f.

LaTeX

$$$\big(\mathrm{iSup}\,s\big)\map f = \big(\bigsqcup_i (s(i)\map f)\big)$$$

Lean4

@[to_additive]
theorem map_iSup {ι : Sort*} (f : F) (s : ι → Submonoid M) : (iSup s).map f = ⨆ i, (s i).map f :=
  (gc_map_comap f : GaloisConnection (map f) (comap f)).l_iSup

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