map_iSup — Mathlib

English

Image of a supremum along f equals the supremum of the images: map f (iSup s) = iSup (map f (s i)).

Русский

Образ наибольшего по индексу через f равен наибольшему образов по индексу: map f (iSup s) = iSup (map f (s i)).

LaTeX

$$$\\operatorname{map}_f\\left(\\iSup_i s(i)\\right) = \\iSup_i \\operatorname{map}_f(s(i))$$$

Lean4

theorem map_iSup {ι : Sort*} (f : F) (s : ι → NonUnitalSubsemiring R) :
    (map f (iSup s) : NonUnitalSubsemiring S) = ⨆ i, map f (s i) :=
  @GaloisConnection.l_iSup _ _ _ _ _ _ _ (gc_map_comap f) s

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