eq_top_of_neBot — Mathlib

English

If α is a subsingleton and l is a nontrivial filter on α, then l = ⊤.

Русский

Если α является подсинглтон, и l — неботовый фильтр на α, то l = ⊤.

LaTeX

$$[Subsingleton α] l ≠ ⊥ → l = ⊤$$

Lean4

/-- There are only two filters on a `Subsingleton`: `⊥` and `⊤`. If the type is empty, then they are
equal. -/
theorem eq_top_of_neBot [Subsingleton α] (l : Filter α) [NeBot l] : l = ⊤ :=
  by
  refine top_unique fun s hs => ?_
  obtain rfl : s = univ := Subsingleton.eq_univ_of_nonempty (nonempty_of_mem hs)
  exact univ_mem

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