comap_sInf' — Mathlib

English

An alternative expression of comap over InfSet: (sInf s).comap f = ⨅ I ∈ comap f '' s, I.

Русский

Альтернативная запись прообраза над InfSet: (sInf s).comap f = ⨅ I ∈ comap f '' s, I.

LaTeX

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

Lean4

theorem comap_sInf' (s : Set (Ideal S)) : (sInf s).comap f = ⨅ I ∈ comap f '' s, I :=
  _root_.trans (comap_sInf f s) (by rw [iInf_image])

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