mem_coLindelof' — Mathlib

English

Alternatively, s ∈ coLindelof(X) iff there exists t with IsLindelof t and s^c ⊆ t.

Русский

Иначе, s ∈ coLindelof(X) эквивалентно существованию t с IsLindelof t и s^c ⊆ t.

LaTeX

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

Lean4

theorem mem_coLindelof' : s ∈ coLindelof X ↔ ∃ t, IsLindelof t ∧ sᶜ ⊆ t :=
  mem_coLindelof.trans <| exists_congr fun _ => and_congr_right fun _ => compl_subset_comm

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