comap_of_range_mem — Mathlib

English

If a filter f is nontrivial and the range of m is contained in f, then comap m f is nontrivial.

Русский

Если фильтр f нетривиален и диапазон m содержится в f, то comap m f нетривиален.

LaTeX

$$$\operatorname{NeBot}(\operatorname{comap} m f) \iff \exists t \in f, t \cap \operatorname{range}(m) \neq \varnothing$$$

Lean4

theorem comap_of_range_mem {f : Filter β} {m : α → β} (_ : NeBot f) (hm : range m ∈ f) : NeBot (comap m f) :=
  comap_neBot_iff_frequently.2 <| Eventually.frequently hm

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