mem_coLindelof — Mathlib

English

An element s belongs to coLindelof(X) if and only if there exists a Lindelöf set t with t^c ⊆ s.

Русский

Элемент s принадлежит coLindelof(X) тогда и только тогда, когда существует Линдельоф-множество t such that t^c ⊆ s.

LaTeX

$$$s \in \mathrm{coLindelof}(X) \iff \exists t, \mathrm{IsLindelof}(t) \wedge t^c \subseteq s$$$

Lean4

theorem mem_coLindelof : s ∈ coLindelof X ↔ ∃ t, IsLindelof t ∧ tᶜ ⊆ s :=
  hasBasis_coLindelof.mem_iff

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