cofinite_eq_atTop — Mathlib

English

On the natural numbers, the cofinite filter coincides with the atTop filter: cofinite = atTop.

Русский

Для натуральных чисел кофинитный фильтр совпадает с фильтром atTop: cofinite = atTop.

LaTeX

$$$\\operatorname{cofinite} = \\operatorname{atTop}$$$

Lean4

/-- For natural numbers the filters `Filter.cofinite` and `Filter.atTop` coincide. -/
theorem cofinite_eq_atTop : @cofinite ℕ = atTop :=
  by
  refine le_antisymm ?_ atTop_le_cofinite
  refine atTop_basis.ge_iff.2 fun N _ => ?_
  simpa only [mem_cofinite, compl_Ici] using finite_lt_nat N

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