English
If a filter is disjoint from the cocompact filter, its image under a continuous function is also disjoint from the cocompact filter.
Русский
Если фильтр диссоциирован с кокофакт-фильтром, то его образ при непрерывном отображении тоже диссоциирован с кокофакт-фильтром.
LaTeX
$$Disjoint(map g f) (cocompact Y)$$
Lean4
/-- If a filter is disjoint from the cocompact filter, so is its image under any continuous
function. -/
theorem disjoint_map_cocompact {g : X → Y} {f : Filter X} (hg : Continuous g) (hf : Disjoint f (Filter.cocompact X)) :
Disjoint (map g f) (Filter.cocompact Y) :=
by
rw [← Filter.disjoint_comap_iff_map, disjoint_iff_inf_le]
calc
f ⊓ (comap g (cocompact Y))
_ ≤ f ⊓ Filter.cocompact X := (inf_le_inf_left f (Filter.comap_cocompact_le hg))
_ = ⊥ := disjoint_iff.mp hf
