Theorems · Theorem · general topology

IsCompact.induction_on

∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
  IsCompact s →
    ∀ {p : Set X → Prop},
      p ∅ →
        (∀ ⦃s t : Set X⦄, s ⊆ t → p t → p s) →
          (∀ ⦃s t : Set X⦄, p s → p t → p (s ∪ t)) → (∀ 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 compact set s has a neighborhood t within s such that p t, then p s holds.

Defined in

Mathlib.Topology.Compactness.Compact

Cited by

18 results in Mathlib

Foundations

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

Assumes

TopologicalSpace