Documentation Verification Report

CompareReals

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

Statistics

Metric	Count
Definitions `uniformSpace`, `Bourbakiℝ`, `Q`, `bourbakiPkg`, `compareEquiv`, `instCommRingQ`, `instInhabitedBourbakiℝ`, `instInhabitedQ`, `uniformSpace`, `rationalCauSeqPkg`	10
Theorems `compare_uc`, `compare_uc_symm`, `uniformSpace_eq`	3
Total	13

CompareReals

Definitions

Name	Category	Theorems
`Bourbakiℝ` 📖	CompOp	2 math math: `compare_uc_symm`, `compare_uc`
`Q` 📖	CompOp	—
`bourbakiPkg` 📖	CompOp	—
`compareEquiv` 📖	CompOp	2 math math: `compare_uc_symm`, `compare_uc`
`instCommRingQ` 📖	CompOp	—
`instInhabitedBourbakiℝ` 📖	CompOp	—
`instInhabitedQ` 📖	CompOp	—
`uniformSpace` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compare_uc` 📖	mathematical	—	`UniformContinuous` `Bourbakiℝ` `Real` `Bourbaki.uniformSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `DFunLike.coe` `UniformEquiv` `EquivLike.toFunLike` `UniformEquiv.instEquivLike` `compareEquiv`	—	`AbstractCompletion.uniformContinuous_compareEquiv`
`compare_uc_symm` 📖	mathematical	—	`UniformContinuous` `Real` `Bourbakiℝ` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Bourbaki.uniformSpace` `DFunLike.coe` `UniformEquiv` `EquivLike.toFunLike` `UniformEquiv.instEquivLike` `UniformEquiv.symm` `compareEquiv`	—	`AbstractCompletion.uniformContinuous_compareEquiv_symm`

CompareReals.Bourbaki

Definitions

Name	Category	Theorems
`uniformSpace` 📖	CompOp	2 math math: `CompareReals.compare_uc_symm`, `CompareReals.compare_uc`

Rat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`uniformSpace_eq` 📖	mathematical	—	`AbsoluteValue.uniformSpace` `instField` `linearOrder` `instIsStrictOrderedRing` `commRing` `AbsoluteValue.abs` `DivisionRing.toRing` `instDivisionRing` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `instMetricSpace`	—	`UniformSpace.ext` `instIsStrictOrderedRing` `Filter.ext` `Filter.HasBasis.mem_iff` `AbsoluteValue.hasBasis_uniformity` `Metric.uniformity_basis_dist_rat` `abs_sub_comm` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing`

(root)

Definitions

Name	Category	Theorems
`rationalCauSeqPkg` 📖	CompOp	—

---

← Back to Index