atTop_le_cofinite — Mathlib

English

If α has no top element, then the atTop filter is contained in the cofinite filter.

Русский

Пусть у α нет максимального элемента, тогда фильтр atTop вложен в cofinite.

LaTeX

$$$[Preorder\;\alpha]\ [NoTopOrder\;\alpha] \Rightarrow (atTop \le \operatorname{cofinite})$$$

Lean4

/-- If `α` is a preorder with no top element, then `atTop ≤ cofinite`. -/
theorem atTop_le_cofinite [Preorder α] [NoTopOrder α] : (atTop : Filter α) ≤ cofinite :=
  le_cofinite_iff_eventually_ne.mpr eventually_ne_atTop

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