comap_neBot_iff_frequently — Mathlib

English

Equivalently, comap m f is nontrivial exactly when the complement of the range of m is not in f.

Русский

Эквивалентно, comap m f нетривиален тогда и только тогда, когда комплемент диапазона m не принадлежит f.

LaTeX

$$$\operatorname{NeBot}(\operatorname{comap} m f) \iff (\operatorname{range}(m))^{c} \notin f$$$

Lean4

theorem comap_neBot_iff_frequently {f : Filter β} {m : α → β} : NeBot (comap m f) ↔ ∃ᶠ y in f, y ∈ range m := by
  simp only [comap_neBot_iff, frequently_iff, mem_range, @and_comm (_ ∈ _), exists_exists_eq_and]

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