Theorems · Theorem · general topology
WeaklyLocallyCompactSpace.exists_compact_mem_nhds
∀ {X : Type u_3} {inst : TopologicalSpace X} [self : WeaklyLocallyCompactSpace X] (x : X), ∃ s, IsCompact s ∧ s ∈ nhds xEvery point of a weakly locally compact space admits a compact neighborhood.
- Defined in
- Mathlib.Topology.Defs.Filter
- Cited by
- 28 results in Mathlib
- Foundations
- Depth 50 from the axioms · uses propext, Quot.sound
- Assumes
- WeaklyLocallyCompactSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- TopologicalSpacestatement and proof · cited by 24,529
- Filterstatement · cited by 8,121
- nhdsstatement · cited by 5,554
- IsCompactstatement · cited by 1,282
- WeaklyLocallyCompactSpacestatement and proof · cited by 35
Cited by28
Results whose statement or proof uses this declaration.
- exists_continuous_nonneg_posproof · cited by 15
- FiniteDimensional.of_locallyCompactSpaceproof · cited by 7
- exists_compact_supersetproof · cited by 6
- isCompactOperator_id_iff_locallyCompactSpaceproof · cited by 3
- ProperlyDiscontinuousSMul.exists_nhds_image_smul_eq_selfproof · cited by 3
- ProperlyDiscontinuousVAdd.exists_nhds_image_vadd_eq_selfproof · cited by 3
- MeasureTheory.continuousOn_convolution_right_with_paramproof · cited by 2
- RestrictedProduct.weaklyLocallyCompactSpace_of_principalproof · cited by 1
- MeasureTheory.continuous_integral_apply_inv_mulproof · cited by 1
- Continuous.discrete_of_tendsto_cofinite_cocompactproof · cited by 1
- MeasureTheory.locallyIntegrable_iffproof · cited by 1
- MeasureTheory.continuous_integral_apply_neg_addproof · cited by 1