instOrderBot — Mathlib

English

There is a bottom element in the lattice of PFilters whenever P has a top element, given by ⟨⊥⟩.

Русский

Если у P имеется верхняя граница, существует нижний элемент в пространстве PFilter, заданный ⟨⊥⟩.

LaTeX

$$$$ \\bot_{PFilter(P)} = \\langle \\bot \\rangle. $$$$

Lean4

/-- There is a bottom filter when `P` has a top element. -/
instance : OrderBot (PFilter P) where
  bot := ⟨⊥⟩
  bot_le F := (bot_le : ⊥ ≤ F.dual)

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