limsSup_top — Mathlib

English

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

Русский

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

LaTeX

$$$\\limsSup (\\top : Filter \\alpha) = \\top$$$

Lean4

@[simp]
theorem limsSup_top : limsSup (⊤ : Filter α) = ⊤ :=
  top_unique <| le_sInf <| by simpa [eq_univ_iff_forall] using fun b hb => top_unique <| hb _

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