comap_neBot_iff_compl_range — Mathlib

English

The equivalence comap_neBot_iff_compl_range states that NeBot comap m f is equivalent to the complement of range m not being in f.

Русский

Эквивалентность comap_neBot_iff_compl_range говорит, что NeBot comap m f эквивалентно тому, что комплемент диапазона m не принадлежит f.

LaTeX

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

Lean4

theorem comap_neBot_iff_compl_range {f : Filter β} {m : α → β} : NeBot (comap m f) ↔ (range m)ᶜ ∉ f :=
  comap_neBot_iff_frequently

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