comap_of_surj — Mathlib

English

If f is a nontrivial filter on β and m: α → β is surjective, then the pullback of f along m is nontrivial.

Русский

Пусть f — непустой фильтр на β и m: α → β сюръективно; тогда обратный образ фильтра f по m не пустой.

LaTeX

$$NeBot f ∧ Surjective m ⇒ NeBot (comap m f)$$

Lean4

theorem comap_of_surj {f : Filter β} {m : α → β} (hf : NeBot f) (hm : Surjective m) : NeBot (comap m f) :=
  hf.comap_of_range_mem <| univ_mem' hm

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