neBot_inf_comap_iff_map — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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