coLindelof_le_coclosedLindelof — Mathlib

English

The coLindelöf filter is contained in the coclosedLindelöf filter: every coLindelöf set has a coclosed Lindelöf superset.

Русский

Фильтр coLindelof содержится в coclosedLindelof: каждоe множество из coLindelof имеет надмножество coclosed Lindelöf.

LaTeX

$$$coLindelof X \le coclosedLindelof X$$$

Lean4

theorem coLindelof_le_coclosedLindelof : coLindelof X ≤ coclosedLindelof X :=
  iInf_mono fun _ => le_iInf fun _ => le_rfl

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