Theorems · Theorem · general topology
IsCompact.elim_nhds_subcover
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
IsCompact s → ∀ (U : X → Set X), (∀ x ∈ s, U x ∈ nhds x) → ∃ t, (∀ x ∈ t, x ∈ s) ∧ s ⊆ ⋃ x ∈ t, U x- Defined in
- Mathlib.Topology.Compactness.Compact
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- TopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
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
- Finsetstatement and proof · cited by 13,712
- Filterstatement · cited by 8,121
- nhdsstatement and proof · cited by 5,554
- Set.iUnionstatement and proof · cited by 2,483
- IsCompactstatement and proof · cited by 1,282
- nhdsSetproof · cited by 267
- subset_of_mem_nhdsSetproof · cited by 10
- IsCompact.elim_nhds_subcover_nhdsSetproof · cited by 2
Cited by15
Results whose statement or proof uses this declaration.
- exists_compact_supersetproof · cited by 6
- IsCompact.disjoint_nhdsSet_leftproof · cited by 6
- CompactSpace.elim_nhds_subcoverproof · cited by 5
- LocallyFinite.finite_nonempty_inter_compactproof · cited by 4
- IsCompact.finite_of_discreteproof · cited by 4
- finite_cover_balls_of_compactproof · cited by 2
- Topology.IsLocallyConstructible.isConstructible_of_subset_of_isCompactproof · cited by 2
- Dynamics.exists_isDynCoverOf_of_isCompact_invariantproof · cited by 2
- AffineSpace.cobounded_eq_iSup_sphere_asymptoticNhdsproof · cited by 1
- countable_cover_nhdsWithin_of_sigmaCompactproof · cited by 1
- Dynamics.exists_isDynCoverOf_of_isCompact_uniformContinuousproof · cited by 1
- TopologicalSpace.Clopens.exists_finset_eq_sup_prodproof · cited by 1