map_inf_le — Mathlib

English

For filters f and g, map m of their infimum is below the infimum of their mapped images.

Русский

Для фильтров f и g отображение map m от их наименьшего есть ниже наименьшего от отображений.

LaTeX

$$map_inf_le {f g : Filter α} {m : α → β} : map m (f ⊓ g) ≤ map m f ⊓ map m g$$

Lean4

theorem map_inf_le {f g : Filter α} {m : α → β} : map m (f ⊓ g) ≤ map m f ⊓ map m g :=
  (@map_mono _ _ m).map_inf_le f g

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