map_iInf_comap_of_surjective — Mathlib

English

Same as map_iInf_comap_of_surjective: map f (iInf S) = iInf (map f ∘ S).

Русский

То же: образ над пересечением предобразов равен пересечению образов.

LaTeX

$$$\operatorname{map} f (\bigwedge_i (S i \operatorname{comap} f)) = \bigwedge_i S i$$$

Lean4

theorem map_iInf_comap_of_surjective {ι : Sort*} (S : ι → Submodule R₂ M₂) : (⨅ i, (S i).comap f).map f = iInf S :=
  (giMapComap hf).l_iInf_u _

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