disjoint_of_map — Mathlib

English

If the images of two filters under a function are disjoint, then the original filters are disjoint.

Русский

Если образ(ы) двух фильтров под функцией попарно непересекаются, то сами фильтры пересечения не имеют.

LaTeX

$$Disjoint (map f F) (map f G) → Disjoint F G$$

Lean4

theorem disjoint_of_map {α β : Type*} {F G : Filter α} {f : α → β} (h : Disjoint (map f F) (map f G)) : Disjoint F G :=
  disjoint_iff.mpr <| map_eq_bot_iff.mp <| le_bot_iff.mp <| trans map_inf_le (disjoint_iff.mp h)

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