disjoint_comap_iff_map' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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