comap_iInf — Mathlib

English

The comap distributes over indexed infimum: (iInf s).comap f = ⨅ i, (s i).comap f.

Русский

Предобраз распределяется по индексированному инфиминуму: (iInf s).comap f = ⨅ i, (s i).comap f.

LaTeX

$$$ (\mathrm{iInf}\,s).{\mathrm{comap}}\!\_f = \big(\inf_i (s(i).{\mathrm{comap}}\!_f)\big)$$$

Lean4

@[to_additive]
theorem comap_iInf {ι : Sort*} (f : F) (s : ι → Submonoid N) : (iInf s).comap f = ⨅ i, (s i).comap f :=
  (gc_map_comap f : GaloisConnection (map f) (comap f)).u_iInf

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