comap_iInf_map_of_injective — Mathlib

English

For any S: ι → Subsemigroup M, the comap of the infimum of the image under f equals the infimum of the comaps: (iInf (S i).map f).comap f = iInf S.

Русский

Для семейства S_i подполугрупп M, комапа инфимума образов под f равна инфимуму комап: (iInf_i S_i).map f).comap f = iInf S_i.

LaTeX

$$(iInf i => (S i).map f).comap f = iInf S$$

Lean4

@[to_additive]
theorem comap_iInf_map_of_injective (S : ι → Subsemigroup M) : (⨅ i, (S i).map f).comap f = iInf S :=
  (gciMapComap hf).u_iInf_l _

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