Structures · Topology
CompleteSpace
A complete space is defined here using uniformities. A uniform space is complete if every Cauchy filter converges.
- Defined in
- Mathlib.Topology.UniformSpace.Cauchy
- Shape
- One type argument · adds complete
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by5
Concrete types that are instances47
- Real
- Complex
- SeparationQuotient
- NNReal
- ContinuousLinearMap
- BoundedContinuousFunction
- Padic
- CStarMatrix
- UniformSpace.Completion
- Quaternion
- Unitization
- IsDedekindDomain.HeightOneSpectrum.adicCompletion
- Matrix
- NumberField.InfinitePlace.Completion
- PadicInt
- WithLp
- TrivSqZeroExt
- UniformFun
- DoubleCentralizer
- UniformOnFun
- ContinuousMapZero
- ZeroAtInftyContinuousMap
- ContinuousAlternatingMap
- TopologicalSpace.NonemptyCompacts
- WithCStarModule
- ContinuousMultilinearMap
- TopologicalSpace.Compacts
- PiLp
- SemiNormedGrp.carrier
- TopologicalSpace.Closeds
- Path
- ODE.FunSpace
- GromovHausdorff.GHSpace
- TopologicalSpace.Opens.CompleteCopy
- CauchyFilter
- LaurentSeries
- UniformSpaceCat.carrier
- CpltSepUniformSpace.α
- Subtype
- Prod
- Set.Elem
- ULift
- MulOpposite
- AddOpposite
- HasQuotient.Quotient
- ContinuousMap
- Sum
How is a type an instance?
Loading the hierarchy index…
Assumed by2,650
- ContinuousLinearMap.adjoint
- MeasureTheory.integral_const
- InnerProductSpace.toDual
- MeasureTheory.L1.setToL1
- LinearMap.toContinuousLinearMap
- Summable.of_norm
- MeasureTheory.condExpL2
- intervalIntegral.integral_const
- ContinuousLinearMap.integral_comp_comm
- ImplicitFunctionData.pt
- FiniteDimensional.complete
- MeasureTheory.integrable_condExp
- MeasureTheory.L1.integral
- ImplicitFunctionData.implicitFunction
- LinearEquiv.toContinuousLinearEquiv
- Summable.of_norm_bounded
- HasGradientAt
- ImplicitFunctionData.leftFun
- ImplicitFunctionData.rightFun
- Summable.comp_injective
- DifferentiableOn.analyticOnNhd
- MeasureTheory.setToFun_eq
- MeasureTheory.integral_dirac
- HasGradientWithinAt
- IsClosed.isComplete
- selfAdjoint.expUnitary
- gradient
- CompleteSpace.complete
- MvPowerSeries.aeval
- MeasureTheory.Lp.toTemperedDistribution
- ContinuousLinearMap.adjoint_inner_left
- ContinuousLinearMap.adjoint_adjoint
- Module.Basis.equivFunL
- MeasureTheory.condExp_congr_ae
- RKHS.kerFun
- LinearMap.continuous_of_finiteDimensional
- integral_smul_const
- ImplicitFunctionData.prodFun
- MeasureTheory.L1.integralCLM
- HasStrictFDerivAt.toOpenPartialHomeomorph
- TemperedDistribution.MemSobolev
- Summable.subtype
- ProperCone.innerDual
- MeasureTheory.setIntegral_const
- Isometry.isClosedEmbedding
- MeasureTheory.L1.integral_def
- Summable.of_norm_bounded_eventually
- ProbabilityTheory.HasGaussianLaw.memLp_two
- MeasureTheory.setIntegral_condExp
- LinearPMap.adjoint
Ancestors0
No ancestors.