Theorems · Inductive type · general topology
TopologicalSpace.PositiveCompacts
(α : Type u_4) → [TopologicalSpace α] → Type u_4
The type of compact sets with nonempty interior of a topological space.
See also TopologicalSpace.Compacts and TopologicalSpace.NonemptyCompacts.
- Defined in
- Mathlib.Topology.Sets.Compacts
- Cited by
- 112 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 2 definitions · uses no axioms
- Assumes
- TopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement · cited by 24,529
Cited by133
Results whose statement or proof uses this declaration.
- MeasureTheory.Measure.addHaarproof · cited by 26
- MeasureTheory.Measure.addHaarMeasurestatement and proof · cited by 21
- TopologicalSpace.PositiveCompacts.isCompactstatement and proof · cited by 21
- TopologicalSpace.PositiveCompacts.interior_nonemptystatement and proof · cited by 15
- TopologicalSpace.PositiveCompacts.toCompactsstatement and proof · cited by 14
- MeasureTheory.Measure.haar.chaarstatement and proof · cited by 12
- Module.Basis.parallelepipedstatement · cited by 12
- MeasureTheory.Measure.haarproof · cited by 11
- MeasureTheory.Measure.haar.addCHaarstatement and proof · cited by 11
- MeasureTheory.Measure.haarMeasurestatement and proof · cited by 10
- MeasureTheory.Measure.addHaarMeasure_uniquestatement and proof · cited by 9
- MeasureTheory.Measure.haar.haarContentstatement and proof · cited by 8