Structures · Topology
CompactSpace
Type class for compact spaces. Separation is sometimes included in the definition, especially in the French literature, but we do not include it here.
- Defined in
- Mathlib.Topology.Defs.Filter
- Shape
- One type argument · adds isCompact_univ
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by5
Forgetful instances
Provided automatically by
Concrete types that are instances45
- Quiver.Hom
- TopCat.carrier
- DomMulAct
- PadicInt
- Units
- DomAddAct
- AddUnits
- TopologicalSpace.NonemptyCompacts
- AlgEquiv
- PrimeSpectrum
- TopologicalSpace.Compacts
- AddCircle
- PontryaginDual
- Circle
- SingularManifold.M
- ContinuousAddMonoidHom
- ContinuousMonoidHom
- CategoryTheory.Aut
- TopologicalSpace.Closeds
- OnePoint
- ConnectedComponents
- ZerothHomotopy
- Ultrafilter
- FirstOrder.Language.Theory.CompleteType
- MeasureTheory.ProbabilityMeasure
- GromovHausdorff.GHSpace.Rep
- GromovHausdorff.OptimalGHCoupling
- StoneCech
- PreStoneCech
- CategoryTheory.Monad.Algebra.A
- WithConstructibleTopology
- Subtype
- Prod
- Set.Elem
- ULift
- MulOpposite
- AddOpposite
- HasQuotient.Quotient
- Sum
- Multiplicative
- Additive
- Sigma
- Set
- Quotient
- Quot
How is a type an instance?
Loading the hierarchy index…
Assumed by699
- isCompact_univ
- IsClosed.isCompact
- CompHausLike.of
- isCompact_range
- BoundedContinuousFunction.mkOfCompact
- ContinuousMap.toLp
- LightProfinite.of
- ContinuousMap.norm_coe_le_norm
- CompactSpace.isCompact_univ
- ContinuousMap.norm_le
- CompHaus.of
- AlgebraicGeometry.Scheme.OpenCover.finiteSubcover
- Profinite.of
- CompHausLike.ofHom
- ContinuousMap.equivBoundedOfCompact
- ContinuousMap.linearIsometryBoundedOfCompact
- Continuous.isClosedMap
- GromovHausdorff.toGHSpace
- ContinuousMap.isometryEquivBoundedOfCompact
- ProfiniteGrp.of
- AlgebraicGeometry.QuasiCompact.compactSpace_of_compactSpace
- GromovHausdorff.ghDist
- ProfiniteAddGrp.of
- finite_of_compact_of_discrete
- stoneCechExtend
- GromovHausdorff.OptimalGHCoupling
- ProfiniteGrp.exist_openNormalSubgroup_sub_open_nhds_of_one
- CompHausLike.sigmaComparison
- CompactSpace.elim_nhds_subcover
- ProfiniteGrp.ofHom
- ProfiniteAddGrp.ofHom
- AlgebraicGeometry.exists_map_eq_top
- CompactSpace.uniformContinuous_of_continuous
- Continuous.isClosedEmbedding
- isTopologicalBasis_isClopen
- Filter.cocompact_eq_bot
- ContinuousMap.attachBound
- ContinuousMapZero.hasFiniteIntegral_mkD_restrict_of_bound
- ContinuousMap.norm_eq_iSup_norm
- ContinuousMap.starSubalgebra_topologicalClosure_eq_top_of_separatesPoints
- ContinuousMapZero.induction_on_of_compact
- ContinuousMapZero.UniqueHom.eq_of_continuous_of_map_id
- GromovHausdorff.optimalGHInjl
- GromovHausdorff.optimalGHInjr
- stoneCechExtend_extends
- ContinuousMap.hasFiniteIntegral_mkD_restrict_of_bound
- AlgebraicGeometry.ExistsHomHomCompEqCompAux.i'
- ContinuousMap.addEquivBoundedOfCompact
- polynomialFunctions.starClosure_topologicalClosure
- NonemptyCompacts.kuratowskiEmbedding
Ancestors0
No ancestors.