comap_neBot — Mathlib

English

The nontriviality of comap m f is equivalent to the complement of the range of m not being 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 {f : Filter β} {m : α → β} (hm : ∀ t ∈ f, ∃ a, m a ∈ t) : NeBot (comap m f) :=
  comap_neBot_iff.mpr hm

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