comap_of_image_mem — Mathlib

English

If f is a nontrivial filter on β and m: α → β has a set s with m''s ∈ f, then the pullback of f along m is nontrivial.

Русский

Пусть f — непустой фильтр на β и существует множество s ⊆ α such that m[s] ∈ f; тогда обратный образ фильтра f по m не пустой.

LaTeX

$$NeBot f ⇒ (m''s ∈ f) ⇒ NeBot (comap m f)$$

Lean4

theorem comap_of_image_mem {f : Filter β} {m : α → β} (hf : NeBot f) {s : Set α} (hs : m '' s ∈ f) :
    NeBot (comap m f) :=
  hf.comap_of_range_mem <| mem_of_superset hs (image_subset_range _ _)

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