hyperfilter_le_atTop — Mathlib

English

The hyperfilter on the natural numbers is below the atTop filter: (hyperfilter ℕ).toFilter ≤ atTop.

Русский

Гиперфильтр на множествах натуральных чисел лежит ниже фильтра atTop: (hyperfilter ℕ).toFilter ≤ atTop.

LaTeX

$$$(\text{hyperfilter } \mathbb{N}).toFilter \leq \text{atTop}$$$

Lean4

theorem _root_.Nat.hyperfilter_le_atTop : (hyperfilter ℕ).toFilter ≤ atTop :=
  hyperfilter_le_cofinite.trans_eq Nat.cofinite_eq_atTop

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