map_iSup — Mathlib

English

The image of an infimum over a family of ideals commutes: map f (iInf K) = iInf_i map f (K i).

Русский

Образ пересечения над семейством идеалов коммутирует: map f (iInf K) = iInf_i map f (K i).

LaTeX

$$$\\operatorname{map} f\\bigl(\\bigwedge_i K_i\\bigr) = \\bigwedge_i \\operatorname{map} f(K_i)$$$

Lean4

theorem map_iSup (K : ι → Ideal R) : (iSup K).map f = ⨆ i, (K i).map f :=
  (gc_map_comap f : GaloisConnection (map f) (comap f)).l_iSup

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