neBot_inf_comap_iff_map' — Mathlib

English

Let f: α → β be a function and F a filter on α, G a filter on β. Then NeBot (comap f G ⊓ F) is equivalent to NeBot (G ⊓ map f F).

Русский

Пусть f: α → β, фильтры F на α и G на β. Тогда NeBot (comap f G ⊓ F) эквивалентно NeBot (G ⊓ map f F).

LaTeX

$$$ \operatorname{NeBot} (\operatorname{comap} f G \inf F) \iff \operatorname{NeBot} (G \inf \operatorname{map} f F) $$$

Lean4

theorem neBot_inf_comap_iff_map' {f : α → β} {F : Filter α} {G : Filter β} :
    NeBot (comap f G ⊓ F) ↔ NeBot (G ⊓ map f F) := by rw [← map_neBot_iff, Filter.push_pull']

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