map_iInf_comap_of_surjective — Mathlib

English

Let f be surjective. For any ι, the image under f of the infimum over i of (K(i).comap f) equals the infimum over i of K(i): map f (⊓_i (K(i).comap f)) = ⊓_i K(i).

Русский

Пусть f сюръективно. Тогда map f от пересечения предобразов равняется пересечению самих K(i).

LaTeX

$$$hf : \mathrm{Function.Surjective}(f) \rightarrow \forall K : ι \to \mathrm{Ideal}(S), \; (\bigwedge_i (K(i).comap f)).map f = \bigwedge_i K(i)$$$

Lean4

theorem map_iInf_comap_of_surjective (K : ι → Ideal S) : (⨅ i, (K i).comap f).map f = iInf K :=
  (giMapComap f hf).l_iInf_u _

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