Theorems · Theorem · general topology

IsCompact.nonempty_inter_sInter

∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
  IsCompact s →
    ∀ {t : Set (Set X)}, (∀ a ∈ t, IsClosed a) → (∀ a ⊆ t, a.Finite → (s ∩ ⋂₀ a).Nonempty) → (s ∩ ⋂₀ t).Nonempty

Defined in: Mathlib.Topology.Compactness.Compact
Cited by: 1 results in Mathlib
Foundations: Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: TopologicalSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites20

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement and proof · cited by 53,352
TopologicalSpacestatement and proof · cited by 24,529
Finsetproof · cited by 13,712
SetLike.coeproof · cited by 8,199
Set.Elemproof · cited by 7,166
Set.imageproof · cited by 5,609
Set.Nonemptystatement and proof · cited by 2,627
Set.Finitestatement and proof · cited by 1,814
IsClosedstatement and proof · cited by 1,639
IsCompactstatement and proof · cited by 1,282
Set.iInterproof · cited by 1,084
Set.sInterstatement and proof · cited by 225

Cited by1

Results whose statement or proof uses this declaration.

CompactSpace.nonempty_sInterproof · cited by 0