comap_sInf — Mathlib

English

Preimage distributes over InfSet: comap f (sInf s) = ⨅ I ∈ s, comap f I.

Русский

Прообраз распределяется по множеству: comap f (sInf s) = ⨅ I ∈ s, comap f I.

LaTeX

$$$\\operatorname{comap} f\\bigl(\\operatorname{sInf} s\\bigr) = \\bigwedge_{I\\in s} \\operatorname{comap} f(I)$$$

Lean4

theorem comap_sInf (s : Set (Ideal S)) : (sInf s).comap f = ⨅ I ∈ s, (I : Ideal S).comap f :=
  (gc_map_comap f : GaloisConnection (map f) (comap f)).u_sInf

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