map_iInf_comap_of_surjective — Mathlib

English

For a family (S i) of submonoids of N, the image under map f of the infimum over i of comaps equals the infimum of the family: map f (iInf_i (comap f (S i))) = iInf_i S.

Русский

Для семейства подмножества S_i моноидов N отображение map f переносит пересечение по индексу через comap: map f (iInf_i (comap f (S_i))) = iInf_i S_i.

LaTeX

$$$ \operatorname{map} f\big(\operatorname{iInf}_i (\operatorname{comap} f (S_i))\big) = \operatorname{iInf}_i S_i. $$$

Lean4

@[to_additive]
theorem map_iInf_comap_of_surjective (S : ι → Submonoid N) : (⨅ i, (S i).comap f).map f = iInf S :=
  (giMapComap hf).l_iInf_u _

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