unique — Mathlib

English

If α is a subsingleton, then there is a unique filter on α; in particular, any nonempty filter equals ⊤.

Русский

Если α является пустым или одиночным типом, существует единственный фильтр на α; в частности, любой непустой фильтр равен ⊤.

LaTeX

$$[Subsingleton α] l ≠ ⊥ → l = ⊤$$

Lean4

/-- There is exactly one filter on an empty type. -/
instance unique [IsEmpty α] : Unique (Filter α) where
  default := ⊥
  uniq := filter_eq_bot_of_isEmpty

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