comap_inf_principal_neBot_of_image_mem

English

If f is a nontrivial filter on β and s ⊆ α with m '' s ∈ f, then NeBot (comap m f ⊓ 𝓟 s).

Русский

Если f не тривиален на β и s ⊆ α удовлетворяет m''s ∈ f, тогда NeBot (comap m f ⊓ 𝓟 s).

LaTeX

$$$ \mathrm{NeBot} (\mathrm{comap} m f \inf \mathcal{P}(s)) $$$

Lean4

theorem comap_inf_principal_neBot_of_image_mem {f : Filter β} {m : α → β} (hf : NeBot f) {s : Set α} (hs : m '' s ∈ f) :
    NeBot (comap m f ⊓ 𝓟 s) :=
  by
  rw [neBot_inf_comap_iff_map', map_principal, ← frequently_mem_iff_neBot]
  exact Eventually.frequently hs

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