atTop_eq — Mathlib

English

If a type α is a subsingleton with a preorder, then the atTop filter on α equals the universal top filter.

Русский

Если тип α деликатно однозначен по порядку, то фильтр atTop на α равен верхнему фильтру ⊤.

LaTeX

$$$$\text{If } [Subsingleton(\alpha)], [Preorder(\alpha)]\;:\; (\text{atTop} : \text{Filter } \alpha) = \top.$$$$

Lean4

@[nontriviality]
theorem atTop_eq (α) [Subsingleton α] [Preorder α] : (atTop : Filter α) = ⊤ :=
  by
  refine top_unique fun s hs x => ?_
  rw [atTop, ciInf_subsingleton x, mem_principal] at hs
  exact hs left_mem_Ici

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