isLindelof_iff_countable_subcover

English

If each K(n) is Lindelöf then Accumulate(K,n) is Lindelöf.

Русский

Если каждый K(n) — Линдельёфово, то Accumulate(K,n) тоже Линдельёфово.

LaTeX

$$$\forall n, IsLindelof(K(n)) \Rightarrow IsLindelof(Accumulate(K,n)).$$$

Lean4

/-- A set `s` is Lindelöf if and only if
for every open cover of `s`, there exists a countable subcover. -/
theorem isLindelof_iff_countable_subcover :
    IsLindelof s ↔
      ∀ {ι : Type u} (U : ι → Set X),
        (∀ i, IsOpen (U i)) → (s ⊆ ⋃ i, U i) → ∃ t : Set ι, t.Countable ∧ s ⊆ ⋃ i ∈ t, U i :=
  ⟨fun hs ↦ hs.elim_countable_subcover, isLindelof_of_countable_subcover⟩

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