disjoint_comap_iff_map — Mathlib

English

Let f: α → β be a function and F a filter on α, G a filter on β. Then F and comap f G are disjoint if and only if map f F and G are disjoint: Disjoint F (comap f G) ↔ Disjoint (map f F) G.

Русский

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

LaTeX

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

Lean4

theorem disjoint_comap_iff_map {f : α → β} {F : Filter α} {G : Filter β} :
    Disjoint F (comap f G) ↔ Disjoint (map f F) G := by simp only [disjoint_iff, ← Filter.push_pull, map_eq_bot_iff]

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