comap_surjective_eq_bot — Mathlib

English

If m is a surjective map, pulling back a filter f along m yields bottom if and only if f is bottom: comap m f = ⊥ ⇔ f = ⊥.

Русский

Если m сюръективно отображает, то обратное изображение фильтра по m даёт ноль тогда и только тогда, когда сам фильтр f является нулём: comap m f = ⊥ ⇔ f = ⊥.

LaTeX

$$$\operatorname{comap}_m f = \bot \iff f = \bot$ (при $\mathrm{Surjective}(m)$)$$

Lean4

theorem comap_surjective_eq_bot {f : Filter β} {m : α → β} (hm : Surjective m) : comap m f = ⊥ ↔ f = ⊥ := by
  rw [comap_eq_bot_iff_compl_range, hm.range_eq, compl_univ, empty_mem_iff_bot]

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