map_iSup — Mathlib

English

For a RingHom f and a family s(i) of Subsemirings, map f of the supremum equals the supremum of the mapped-subsemirings: map f (iSup s) = iSup (map f ∘ s).

Русский

Для кольцевого однородного отображения f и семейства Subsemiring s(i) выполняется: map f (iSup s) = iSup (map f (s)).

LaTeX

$$$\\mathrm{map}\ f\\left(\\iSup i\\, s(i)\\right) = \\iSup i\\, (\\mathrm{map}\ f\\ (s(i)))$$$

Lean4

theorem map_iSup {ι : Sort*} (f : R →+* S) (s : ι → Subsemiring R) : (iSup s).map f = ⨆ i, (s i).map f :=
  (gc_map_comap f).l_iSup

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