coLindelof_le_cofinite — Mathlib

English

The coLindelöf filter is coarser than the cofinite filter: every coLindelöf set contains a cofinite subset.

Русский

Фильтр coLindelof менее тонок, чем фильтр cofinite: каждый элемент coLindelof содержит кофинитное подмножество.

LaTeX

$$$\mathrm{coLindelof}(X) \le \mathrm{cofinite}$$$

Lean4

theorem coLindelof_le_cofinite : coLindelof X ≤ cofinite := fun s hs =>
  compl_compl s ▸ hs.isLindelof.compl_mem_coLindelof

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