comap_iInf — Mathlib

English

For f: R →+* S and a family s(i) of Subsemirings of S, comap f (iInf s) = iInf (comap f (s i)).

Русский

Для отображения f и семейства s(i) подполей S имеем: comap f (iInf s) = iInf (comap f (s(i))).

LaTeX

$$$\\mathrm{comap}\ f\\ (\\iInf\\ i\\; s(i)) = \\iInf\\ i\\; (\\mathrm{comap}\\ f\\ (s(i)))$$$

Lean4

theorem comap_iInf {ι : Sort*} (f : R →+* S) (s : ι → Subsemiring S) : (iInf s).comap f = ⨅ i, (s i).comap f :=
  (gc_map_comap f).u_iInf

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