DiscreteUniformity

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

Statistics

Metric	Count
Definitions DiscreteUniformity	1
Theorems eq_bot, eq_principal_idRel, eq_principal_relId, eq_principal_setRelId, idRel_mem_uniformity, inst, instDiscreteTopology, instProd, relId_mem_uniformity, uniformContinuous, discreteUniformity_iff_eq_bot, discreteUniformity_iff_eq_principal_idRel, discreteUniformity_iff_eq_principal_relId, discreteUniformity_iff_eq_principal_setRelId, discreteUniformity_iff_idRel_mem_uniformity, discreteUniformity_iff_relId_mem_uniformity, discreteUniformity_iff_setRelId_mem_uniformity	17
Total	18

DiscreteUniformity

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_bot 📖	mathematical	—	Bot.bot UniformSpace instBotUniformSpace	—	—
eq_principal_idRel 📖	mathematical	—	uniformity Filter.principal SetRel.id	—	eq_principal_setRelId
eq_principal_relId 📖	mathematical	—	uniformity Filter.principal SetRel.id	—	eq_principal_setRelId
eq_principal_setRelId 📖	mathematical	—	uniformity Filter.principal SetRel.id	—	discreteUniformity_iff_eq_principal_setRelId
idRel_mem_uniformity 📖	mathematical	—	SetRel Filter Filter.instMembership uniformity SetRel.id	—	relId_mem_uniformity
inst 📖	mathematical	—	DiscreteUniformity Bot.bot UniformSpace instBotUniformSpace	—	—
instDiscreteTopology 📖	mathematical	—	DiscreteTopology UniformSpace.toTopologicalSpace	—	eq_bot UniformSpace.toTopologicalSpace_bot
instProd 📖	mathematical	—	DiscreteUniformity instUniformSpaceProd	—	eq_principal_setRelId uniformity_prod_eq_comap_prod Filter.prod_principal_principal Filter.comap_principal
relId_mem_uniformity 📖	mathematical	—	SetRel Filter Filter.instMembership uniformity SetRel.id	—	discreteUniformity_iff_setRelId_mem_uniformity
uniformContinuous 📖	mathematical	—	UniformContinuous	—	eq_bot

(root)

Definitions

Name	Category	Theorems
DiscreteUniformity 📖	CompData	17 math math: discreteUniformity_iff_eq_principal_relId, DiscreteUniformity.instProd, TopologicalSpace.NonemptyCompacts.instDiscreteUniformity, TopologicalSpace.Compacts.discreteUniformity_iff, discreteUniformity_iff_setRelId_mem_uniformity, discreteUniformity_iff_relId_mem_uniformity, discreteUniformity_iff_eq_principal_setRelId, TopologicalSpace.Closeds.instDiscreteUniformity, IsUniformEmbedding.discreteUniformity, discreteUniformity_iff_eq_bot, TopologicalSpace.Compacts.instDiscreteUniformity, discreteUniformity_iff_idRel_mem_uniformity, TopologicalSpace.NonemptyCompacts.discreteUniformity_iff, discreteUniformity_iff_eq_principal_idRel, UniformSpace.hausdorff.instDiscreteUniformitySet, DiscreteUniformity.inst, TopologicalSpace.Closeds.discreteUniformity_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
discreteUniformity_iff_eq_bot 📖	mathematical	—	DiscreteUniformity Bot.bot UniformSpace instBotUniformSpace	—	—
discreteUniformity_iff_eq_principal_idRel 📖	mathematical	—	DiscreteUniformity uniformity Filter.principal SetRel.id	—	discreteUniformity_iff_eq_principal_setRelId
discreteUniformity_iff_eq_principal_relId 📖	mathematical	—	DiscreteUniformity uniformity Filter.principal SetRel.id	—	discreteUniformity_iff_eq_principal_setRelId
discreteUniformity_iff_eq_principal_setRelId 📖	mathematical	—	DiscreteUniformity uniformity Filter.principal SetRel.id	—	discreteUniformity_iff_eq_bot UniformSpace.ext_iff Filter.ext_iff bot_uniformity
discreteUniformity_iff_idRel_mem_uniformity 📖	mathematical	—	DiscreteUniformity SetRel Filter Filter.instMembership uniformity SetRel.id	—	discreteUniformity_iff_setRelId_mem_uniformity
discreteUniformity_iff_relId_mem_uniformity 📖	mathematical	—	DiscreteUniformity SetRel Filter Filter.instMembership uniformity SetRel.id	—	discreteUniformity_iff_setRelId_mem_uniformity
discreteUniformity_iff_setRelId_mem_uniformity 📖	mathematical	—	DiscreteUniformity SetRel Filter Filter.instMembership uniformity SetRel.id	—	UniformSpace.uniformSpace_eq_bot discreteUniformity_iff_eq_bot

---

← Back to Index