mem_coclosedLindelof — Mathlib

English

A set s belongs to coclosedLindelof(X) iff there exists a closed Lindelöf t with t^c ⊆ s.

Русский

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

LaTeX

$$$s \in \mathrm{coclosedLindelof}(X) \iff \exists t, \mathrm{IsClosed}(t) \land \mathrm{IsLindelof}(t) \land t^c \subseteq s$$$

Lean4

theorem mem_coclosedLindelof : s ∈ coclosedLindelof X ↔ ∃ t, IsClosed t ∧ IsLindelof t ∧ tᶜ ⊆ s := by
  simp only [hasBasis_coclosedLindelof.mem_iff, and_assoc]

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