Theorems · Theorem · measure theory
IsCompact.measure_ne_top
∀ {α : Type u_1} {m0 : MeasurableSpace α} [inst : TopologicalSpace α] {μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasureOnCompacts μ] ⦃K : Set α⦄, IsCompact K → μ K ≠ ⊤A compact subset has finite measure for a measure which is finite on compacts.
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 172 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- Setstatement and proof · cited by 53,352
- TopologicalSpacestatement and proof · cited by 24,529
- MeasurableSpacestatement and proof · cited by 13,106
- MeasureTheory.Measurestatement and proof · cited by 10,939
- ENNRealstatement · cited by 9,879
- Top.topstatement · cited by 9,680
- IsCompactstatement and proof · cited by 1,282
- LT.lt.neproof · cited by 872
- MeasureTheory.IsFiniteMeasureOnCompactsstatement and proof · cited by 109
- IsCompact.measure_lt_topproof · cited by 35
Cited by12
Results whose statement or proof uses this declaration.
- MeasureTheory.Measure.addHaarMeasure_uniqueproof · cited by 9
- MeasureTheory.Measure.haarMeasure_uniqueproof · cited by 4
- ContinuousOn.integrableOn_compact'proof · cited by 3
- ProbabilityTheory.BrownianReal.posSemidef_covMatrixproof · cited by 2
- continuousOn_integral_of_compact_supportproof · cited by 2
- tendsto_integral_comp_smul_smul_of_integrableproof · cited by 1
- tendsto_measure_Icc_nhdsWithin_right'proof · cited by 1
- AddMonoidHom.exists_nhds_isBoundedproof · cited by 1
- continuous_parametric_integral_of_continuousproof · cited by 0
- HasCompactSupport.memLp_of_enorm_boundproof · cited by 0
- MonoidHom.exists_nhds_isBoundedproof · cited by 0