limsInf_top — Mathlib

English

In any complete lattice α, the limsInf of the top filter equals the bottom element: limsInf (⊤ : Filter α) = ⊥.

Русский

В любой полной решётке α лиминф верхнего фильтра равен нижнему элементу: limsInf (⊤ : Filter α) = ⊥.

LaTeX

$$$\\operatorname{limsInf}(\\top) = \\bot$$$

Lean4

@[simp]
theorem limsInf_top : limsInf (⊤ : Filter α) = ⊥ :=
  bot_unique <| sSup_le <| by simpa [eq_univ_iff_forall] using fun b hb => bot_unique <| hb _

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