Theorems · Theorem · general topology

IsLindelof.induction_on

∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
  IsLindelof s →
    ∀ {p : Set X → Prop},
      (∀ ⦃s t : Set X⦄, s ⊆ t → p t → p s) →
        (∀ (S : Set (Set X)), S.Countable → (∀ s ∈ S, p s) → p (⋃₀ S)) → (∀ x ∈ s, ∃ t ∈ nhdsWithin x s, p t) → p s

If p : Set X → Prop is stable under restriction and union, and each point x of a Lindelöf set s has a neighborhood t within s such that p t, then p s holds.

Defined in

Mathlib.Topology.Compactness.Lindelof

Cited by

1 results in Mathlib

Foundations

Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpace