top — Mathlib

English

The top filter realizer is obtained by transporting the principal realizer of the universal set via an equality: top = (Realizer.principal univ).ofEq principal_univ.

Русский

Реализатор верхнего фильтра получается из переноса реализатора главного для вселенного множества через равенство: top = (Realizer.principal univ).ofEq principal_univ.

LaTeX

$$$\\text{top} = (\\mathrm{Realizer.principal}\\;\\text{univ}).ofEq\\;\\text{principal\_univ}$.$$

Lean4

/-- `Unit` is a realizer for the top filter -/
protected def top : (⊤ : Filter α).Realizer :=
  (Realizer.principal _).ofEq principal_univ

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