mem_coclosed_Lindelof' — Mathlib

English

The same as mem_coclosedLindelof but with a complementary rearrangement: s ∈ coclosedLindelof ↔ ∃ t closed Lindelöf with s^c ⊆ t.

Русский

То же самое, что mem_coclosedLindelof, но с перестановкой: s ∈ coclosedLindelof ↔ ∃ t замкнутое Линдельоф, s^c ⊆ t.

LaTeX

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

Lean4

theorem mem_coclosed_Lindelof' : s ∈ coclosedLindelof X ↔ ∃ t, IsClosed t ∧ IsLindelof t ∧ sᶜ ⊆ t := by
  simp only [mem_coclosedLindelof, compl_subset_comm]

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