map_eq_bot_iff — Mathlib

English

The image of a filter under a map is bottom exactly when the original filter is bottom.

Русский

Образ фильтра через отображение равен нижнему предельному элементу тогда и только тогда, когда исходный фильтр равен нижнему.

LaTeX

$$map m f = ⊥ ↔ f = ⊥$$

Lean4

@[simp]
theorem map_eq_bot_iff : map m f = ⊥ ↔ f = ⊥ :=
  ⟨by
    rw [← empty_mem_iff_bot, ← empty_mem_iff_bot]
    exact id, fun h => by simp only [h, map_bot]⟩

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