instOrderTopOfOrderBot — Mathlib

English

There is a top element in the PFilter when P has a bottom element, given by ⊤.

Русский

Если P имеет нижнюю границу, в PFilter существует верхняя граница, заданная ⊤.

LaTeX

$$$$ \\text{top}_{PFilter(P)} = \\langle \\top \\rangle. $$$$

Lean4

/-- There is a top filter when `P` has a bottom element. -/
instance {P} [Preorder P] [OrderBot P] : OrderTop (PFilter P)
    where
  top := ⟨⊤⟩
  le_top F := (le_top : F.dual ≤ ⊤)

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