Theorems · Theorem · general topology

IsClosed.exists_minimal_nonempty_closed_subset

∀ {X : Type u} [inst : TopologicalSpace X] [CompactSpace X] {S : Set X},
  IsClosed S → S.Nonempty → ∃ V ⊆ S, V.Nonempty ∧ IsClosed V ∧ ∀ V' ⊆ V, V'.Nonempty → IsClosed V' → V' = V

Defined in

Mathlib.Topology.Compactness.Compact

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceCompactSpace