comap_neBot_iff — Mathlib

English

The nontriviality of comap m f is characterized by the frequently occurring membership of range(m) in f.

Русский

Нетривиальность comap m f характеризуется частым вхождением диапазона m в f.

LaTeX

$$$\operatorname{NeBot}(\operatorname{comap} m f) \iff \exists^{\text{freq}} y \in f, y \in \operatorname{range}(m)$$$

Lean4

theorem comap_neBot_iff {f : Filter β} {m : α → β} : NeBot (comap m f) ↔ ∀ t ∈ f, ∃ a, m a ∈ t :=
  by
  simp only [← forall_mem_nonempty_iff_neBot, mem_comap, forall_exists_index, and_imp]
  exact ⟨fun h t t_in => h (m ⁻¹' t) t t_in Subset.rfl, fun h s t ht hst => (h t ht).imp hst⟩

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