map_iInf_le — Mathlib

English

Map distributes over arbitrary infima: map m of the infimum of a family of filters is below the infimum of the mapped filters.

Русский

Образ через m распределяется по бесконечным минимумам: map m от infimum семейства фильтров лежит под infimum их образов.

LaTeX

$$map m (iInf f) ≤ ⨅ i, map m (f i)$$

Lean4

theorem map_iInf_le {f : ι → Filter α} {m : α → β} : map m (iInf f) ≤ ⨅ i, map m (f i) :=
  le_iInf fun _ => map_mono <| iInf_le _ _

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