UniformSpace

📁 Source: Mathlib/Topology/Category/UniformSpace.lean

Statistics

Metric	Count
Definitions CpltSepUniformSpace, category, concreteCategory, hasForgetToUniformSpace, instCoeSortType, instFunLike, instInhabited, isUniformSpace, of, toUniformSpace, α, UniformSpace, UniformSpaceCat, hom, hom', adj, carrier, completionFunctor, completionHom, extensionHom, hasForgetToTop, instCoeSortType, instConcreteCategorySubtypeForallCarrierUniformContinuous, instFunLike, instInhabited, instLargeCategory, instReflectiveCpltSepUniformSpaceForget₂SubtypeForallαUniformContinuousForallCarrier, ofHom, str	29
Theorems coe_of, completeSpace, hom_comp, hom_id, hom_ofHom, isCompleteSpace, isT0, t0Space, ext, ext_iff, coe_comp, coe_id, coe_mk, coe_of, completionFunctor_map, completionHom_val, extensionHom_val, extension_comp_coe, extension_comp_hom, hom_comp, hom_ext, hom_ext_iff, hom_id, hom_ofHom	24
Total	53

CpltSepUniformSpace

Definitions

Name	Category	Theorems
category 📖	CompOp	7 math math: UniformSpaceCat.completionHom_val, UniformSpaceCat.extension_comp_coe, UniformSpaceCat.completionFunctor_map, hom_comp, UniformSpaceCat.extensionHom_val, UniformSpaceCat.extension_comp_hom, hom_id
concreteCategory 📖	CompOp	7 math math: UniformSpaceCat.completionHom_val, UniformSpaceCat.extension_comp_coe, UniformSpaceCat.completionFunctor_map, hom_comp, UniformSpaceCat.extensionHom_val, UniformSpaceCat.extension_comp_hom, hom_id
hasForgetToUniformSpace 📖	CompOp	4 math math: UniformSpaceCat.completionHom_val, UniformSpaceCat.extension_comp_coe, UniformSpaceCat.extensionHom_val, UniformSpaceCat.extension_comp_hom
instCoeSortType 📖	CompOp	—
instFunLike 📖	CompOp	7 math math: UniformSpaceCat.completionHom_val, UniformSpaceCat.extension_comp_coe, UniformSpaceCat.completionFunctor_map, hom_comp, UniformSpaceCat.extensionHom_val, UniformSpaceCat.extension_comp_hom, hom_id
instInhabited 📖	CompOp	—
isUniformSpace 📖	CompOp	9 math math: UniformSpaceCat.completionHom_val, UniformSpaceCat.extension_comp_coe, isT0, UniformSpaceCat.completionFunctor_map, hom_comp, isCompleteSpace, UniformSpaceCat.extensionHom_val, UniformSpaceCat.extension_comp_hom, hom_id
of 📖	CompOp	2 math math: UniformSpaceCat.completionFunctor_map, coe_of
toUniformSpace 📖	CompOp	5 math math: UniformSpaceCat.extension_comp_coe, t0Space, hom_comp, completeSpace, UniformSpaceCat.extension_comp_hom
α 📖	CompOp	10 math math: UniformSpaceCat.completionHom_val, UniformSpaceCat.extension_comp_coe, isT0, UniformSpaceCat.completionFunctor_map, hom_comp, isCompleteSpace, coe_of, UniformSpaceCat.extensionHom_val, UniformSpaceCat.extension_comp_hom, hom_id

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_of 📖	mathematical	—	α of	—	—
completeSpace 📖	mathematical	—	CompleteSpace UniformSpaceCat.carrier toUniformSpace UniformSpaceCat.str	—	isCompleteSpace
hom_comp 📖	mathematical	—	CategoryTheory.ConcreteCategory.hom CpltSepUniformSpace category UniformContinuous α isUniformSpace instFunLike concreteCategory CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct DFunLike.coe UniformContinuous.comp UniformSpaceCat.carrier toUniformSpace UniformSpaceCat.str UniformSpaceCat.Hom.hom CategoryTheory.InducedCategory.Hom.hom UniformSpaceCat UniformSpaceCat.instLargeCategory Subtype.prop	—	—
hom_id 📖	mathematical	—	CategoryTheory.ConcreteCategory.hom CpltSepUniformSpace category UniformContinuous α isUniformSpace instFunLike concreteCategory CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct uniformContinuous_id	—	—
hom_ofHom 📖	mathematical	—	UniformSpaceCat.Hom.hom UniformSpaceCat.of UniformSpaceCat.ofHom	—	—
isCompleteSpace 📖	mathematical	—	CompleteSpace α isUniformSpace	—	—
isT0 📖	mathematical	—	T0Space α UniformSpace.toTopologicalSpace isUniformSpace	—	—
t0Space 📖	mathematical	—	T0Space UniformSpaceCat.carrier toUniformSpace UniformSpace.toTopologicalSpace UniformSpaceCat.str	—	isT0

UniformSpaceCat

Definitions

Name	Category	Theorems
adj 📖	CompOp	—
carrier 📖	CompOp	14 math math: completionHom_val, hom_ext_iff, extension_comp_coe, CpltSepUniformSpace.t0Space, completionFunctor_map, coe_of, coe_comp, CpltSepUniformSpace.hom_comp, CpltSepUniformSpace.completeSpace, hom_id, coe_id, extensionHom_val, extension_comp_hom, hom_comp
completionFunctor 📖	CompOp	5 math math: completionHom_val, extension_comp_coe, completionFunctor_map, extensionHom_val, extension_comp_hom
completionHom 📖	CompOp	3 math math: completionHom_val, extension_comp_coe, extension_comp_hom
extensionHom 📖	CompOp	3 math math: extension_comp_coe, extensionHom_val, extension_comp_hom
hasForgetToTop 📖	CompOp	—
instCoeSortType 📖	CompOp	—
instConcreteCategorySubtypeForallCarrierUniformContinuous 📖	CompOp	8 math math: completionHom_val, hom_ext_iff, extension_comp_coe, coe_comp, coe_id, extensionHom_val, extension_comp_hom, hom_comp
instFunLike 📖	CompOp	10 math math: completionHom_val, hom_ext_iff, extension_comp_coe, completionFunctor_map, coe_comp, coe_mk, coe_id, extensionHom_val, extension_comp_hom, hom_comp
instInhabited 📖	CompOp	—
instLargeCategory 📖	CompOp	11 math math: completionHom_val, hom_ext_iff, extension_comp_coe, completionFunctor_map, coe_comp, CpltSepUniformSpace.hom_comp, hom_id, coe_id, extensionHom_val, extension_comp_hom, hom_comp
instReflectiveCpltSepUniformSpaceForget₂SubtypeForallαUniformContinuousForallCarrier 📖	CompOp	—
ofHom 📖	CompOp	2 math math: CpltSepUniformSpace.hom_ofHom, hom_ofHom
str 📖	CompOp	13 math math: completionHom_val, hom_ext_iff, extension_comp_coe, CpltSepUniformSpace.t0Space, completionFunctor_map, coe_comp, CpltSepUniformSpace.hom_comp, CpltSepUniformSpace.completeSpace, hom_id, coe_id, extensionHom_val, extension_comp_hom, hom_comp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_comp 📖	mathematical	—	DFunLike.coe carrier instFunLike CategoryTheory.ConcreteCategory.hom UniformSpaceCat instLargeCategory UniformContinuous str instConcreteCategorySubtypeForallCarrierUniformContinuous CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
coe_id 📖	mathematical	—	DFunLike.coe carrier instFunLike CategoryTheory.ConcreteCategory.hom UniformSpaceCat instLargeCategory UniformContinuous str instConcreteCategorySubtypeForallCarrierUniformContinuous CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
coe_mk 📖	mathematical	UniformContinuous carrier str	DFunLike.coe instFunLike Hom.hom	—	—
coe_of 📖	mathematical	—	carrier of	—	—
completionFunctor_map 📖	mathematical	—	CategoryTheory.Functor.map UniformSpaceCat instLargeCategory CpltSepUniformSpace CpltSepUniformSpace.category completionFunctor CategoryTheory.ConcreteCategory.ofHom UniformContinuous CpltSepUniformSpace.α CpltSepUniformSpace.isUniformSpace CpltSepUniformSpace.instFunLike CpltSepUniformSpace.concreteCategory CpltSepUniformSpace.of UniformSpace.Completion carrier str UniformSpace.Completion.uniformSpace UniformSpace.Completion.map DFunLike.coe instFunLike Hom.hom'	—	—
completionHom_val 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj CpltSepUniformSpace CpltSepUniformSpace.category UniformSpaceCat instLargeCategory CategoryTheory.forget₂ UniformContinuous CpltSepUniformSpace.α CpltSepUniformSpace.isUniformSpace CpltSepUniformSpace.instFunLike CpltSepUniformSpace.concreteCategory carrier str instFunLike instConcreteCategorySubtypeForallCarrierUniformContinuous CpltSepUniformSpace.hasForgetToUniformSpace completionFunctor CategoryTheory.ConcreteCategory.hom completionHom UniformSpace.Completion.coe'	—	—
extensionHom_val 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj UniformSpaceCat instLargeCategory CpltSepUniformSpace CpltSepUniformSpace.category completionFunctor CpltSepUniformSpace.α CpltSepUniformSpace.instFunLike CategoryTheory.ConcreteCategory.hom UniformContinuous CpltSepUniformSpace.isUniformSpace CpltSepUniformSpace.concreteCategory extensionHom UniformSpace.Completion.extension carrier str CategoryTheory.forget₂ instFunLike instConcreteCategorySubtypeForallCarrierUniformContinuous CpltSepUniformSpace.hasForgetToUniformSpace	—	—
extension_comp_coe 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom CpltSepUniformSpace UniformSpaceCat instLargeCategory CpltSepUniformSpace.toUniformSpace CategoryTheory.Functor.obj CpltSepUniformSpace.category completionFunctor extensionHom CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.forget₂ UniformContinuous CpltSepUniformSpace.α CpltSepUniformSpace.isUniformSpace CpltSepUniformSpace.instFunLike CpltSepUniformSpace.concreteCategory carrier str instFunLike instConcreteCategorySubtypeForallCarrierUniformContinuous CpltSepUniformSpace.hasForgetToUniformSpace completionHom	—	extension_comp_hom
extension_comp_hom 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom CpltSepUniformSpace UniformSpaceCat instLargeCategory CpltSepUniformSpace.toUniformSpace CategoryTheory.Functor.obj CpltSepUniformSpace.category completionFunctor extensionHom CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.forget₂ UniformContinuous CpltSepUniformSpace.α CpltSepUniformSpace.isUniformSpace CpltSepUniformSpace.instFunLike CpltSepUniformSpace.concreteCategory carrier str instFunLike instConcreteCategorySubtypeForallCarrierUniformContinuous CpltSepUniformSpace.hasForgetToUniformSpace completionHom	—	UniformSpace.Completion.completeSpace UniformSpace.Completion.t0Space hom_ext UniformSpace.Completion.extension_comp_coe CpltSepUniformSpace.t0Space CpltSepUniformSpace.completeSpace
hom_comp 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.comp UniformSpaceCat CategoryTheory.Category.toCategoryStruct instLargeCategory UniformContinuous carrier str DFunLike.coe instFunLike CategoryTheory.ConcreteCategory.hom instConcreteCategorySubtypeForallCarrierUniformContinuous UniformContinuous.comp Subtype.prop	—	—
hom_ext 📖	—	DFunLike.coe carrier instFunLike CategoryTheory.ConcreteCategory.hom UniformSpaceCat instLargeCategory UniformContinuous str instConcreteCategorySubtypeForallCarrierUniformContinuous	—	—	Hom.ext
hom_ext_iff 📖	mathematical	—	DFunLike.coe carrier instFunLike CategoryTheory.ConcreteCategory.hom UniformSpaceCat instLargeCategory UniformContinuous str instConcreteCategorySubtypeForallCarrierUniformContinuous	—	hom_ext
hom_id 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.id UniformSpaceCat CategoryTheory.Category.toCategoryStruct instLargeCategory UniformContinuous carrier str uniformContinuous_id	—	—
hom_ofHom 📖	mathematical	—	Hom.hom of ofHom	—	—

UniformSpaceCat.Hom

Definitions

Name	Category	Theorems
hom 📖	CompOp	6 math math: UniformSpaceCat.coe_mk, CpltSepUniformSpace.hom_ofHom, CpltSepUniformSpace.hom_comp, UniformSpaceCat.hom_id, UniformSpaceCat.hom_ofHom, UniformSpaceCat.hom_comp
hom' 📖	CompOp	2 math math: ext_iff, UniformSpaceCat.completionFunctor_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	hom'	—	—	—
ext_iff 📖	mathematical	—	hom'	—	ext

(root)

Definitions

Name	Category	Theorems
CpltSepUniformSpace 📖	CompData	7 math math: UniformSpaceCat.completionHom_val, UniformSpaceCat.extension_comp_coe, UniformSpaceCat.completionFunctor_map, CpltSepUniformSpace.hom_comp, UniformSpaceCat.extensionHom_val, UniformSpaceCat.extension_comp_hom, CpltSepUniformSpace.hom_id
UniformSpace 📖	CompData	77 math math: Pi.uniformSpace_eq, uniformContinuous_sInf_rng, cauchy_inf_uniformSpace, bot_uniformity, UniformFun.uniformSpace_eq_iInf_precomp_of_cover, isUniformGroup_inf, UniformSpace.toTopologicalSpace_top, isUniformAddGroup_inf, UniformFun.mono, Pi.uniformSpace_comap_precomp, WithAbs.uniformSpace_comap_eq_of_comp, isUniformAddGroup_sInf, uniformContinuous_inf_dom_left₂, cauchy_iInf_uniformSpace', Pi.uniformSpace_comap_restrict, uniformEquicontinuousOn_iInf_rng, Pi.uniformSpace_comap_precomp', uniformEquicontinuous_iInf_rng, ContDiffMapSupportedIn.uniformSpace_eq_iInf, equicontinuous_iInf_rng, UniformConvergenceCLM.uniformSpace_mono, uniformEquicontinuousOn_iInf_dom, le_iff_uniformContinuous_id, DiscreteUniformity.eq_bot, Dynamics.coverEntropy_antitone, UniformContinuous.inf_dom_left, UniformSpace.toTopologicalSpace_bot, uniformContinuous_inf_dom_right₂, UniformSpace.comap_inf, UniformOnFun.uniformSpace_eq_iInf_precomp_of_cover, SeminormFamily.withSeminorms_iff_uniformSpace_eq_iInf, iInf_uniformity, isUniformGroup_sInf, UniformSpace.toTopologicalSpace_sInf, UniformContinuous.inf_dom_right, equicontinuousOn_iInf_rng, Dynamics.coverEntropyInf_antitone, IsUltraUniformity.iInf, isUniformEmbedding_of_spaced_out, UniformSpace.toTopologicalSpace_iInf, CompleteSpace.iInf, UniformSpace.comap_mono, discreteUniformity_iff_eq_bot, UniformSpace.le_def, isUniformAddGroup_iInf, IsUltraUniformity.inf, UniformSpace.uniformSpace_eq_bot, uniformEquicontinuous_iInf_dom, uniformContinuous_iff, Metric.isUniformEmbedding_bot_of_pairwise_le_dist, isUniformGroup_iInf, UniformSpace.comap_iInf, inf_uniformity, Pi.uniformSpace_comap_restrict_sUnion, equicontinuousWithinAt_iInf_rng, UniformOnFun.inf_eq, UniformSpace.toTopologicalSpace_inf, uniformity_eq_of_bilipschitz, UniformOnFun.uniformSpace_eq_inf_precomp_of_cover, IsUltraUniformity.top, uniformContinuous_iInf_rng, UniformFun.iInf_eq, cauchy_iInf_uniformSpace, ContinuousMap.uniformSpace_eq_iInf_precomp_of_cover, UniformFun.uniformSpace_eq_inf_precomp_of_cover, DiscreteUniformity.inst, equicontinuousAt_iInf_rng, uniformContinuous_iInf_dom, Metric.uniformSpace_eq_bot, UniformOnFun.hasBasis_uniformity_of_basis_aux₂, UniformFun.inf_eq, top_uniformity, uniformSpace_comap_id, Filter.HasBasis.uniformSpace_eq_bot, UniformContinuous.inf_rng, UniformOnFun.iInf_eq, ContinuousMap.uniformSpace_eq_inf_precomp_of_cover
UniformSpaceCat 📖	CompData	11 math math: UniformSpaceCat.completionHom_val, UniformSpaceCat.hom_ext_iff, UniformSpaceCat.extension_comp_coe, UniformSpaceCat.completionFunctor_map, UniformSpaceCat.coe_comp, CpltSepUniformSpace.hom_comp, UniformSpaceCat.hom_id, UniformSpaceCat.coe_id, UniformSpaceCat.extensionHom_val, UniformSpaceCat.extension_comp_hom, UniformSpaceCat.hom_comp

---

← Back to Index