Documentation Verification Report

Rat

📁 Source: Mathlib/Topology/Instances/Rat.lean

Statistics

Metric	Count
Definitions `instMetricSpace`, `instMetricSpace`	2
Theorems `dist_cast_rat`, `isClosedEmbedding_coe_rat`, `isUniformEmbedding_coe_rat`, `dist_eq`, `instContinuousInv₀`, `instContinuousSMulNNReal`, `instContinuousSMulOfIsScalarTowerOfRat`, `instContinuousSMulRatReal`, `instContinuousSub`, `instIsTopologicalSemiring`, `instOrderTopology`, `nndist_eq`, `dist_cast_rat`, `isClosedEmbedding_coe_rat`, `isUniformEmbedding_coe_rat`, `continuous_coe_real`, `dist_cast`, `dist_eq`, `instIsTopologicalAddGroup`, `instIsTopologicalRing`, `instIsUniformAddGroup`, `instNoncompactSpace`, `instOrderTopology`, `isDenseEmbedding_coe_real`, `isEmbedding_coe_real`, `isUniformEmbedding_coe_real`, `totallyBounded_Icc`, `uniformContinuous_abs`, `uniformContinuous_add`, `uniformContinuous_coe_real`, `uniformContinuous_neg`	31
Total	33

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dist_cast_rat` 📖	mathematical	—	`Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace` `Rat.instMetricSpace` `instDist`	—	`dist_cast_real` `Rat.dist_cast`
`isClosedEmbedding_coe_rat` 📖	mathematical	—	`Topology.IsClosedEmbedding` `instTopologicalSpaceInt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `Rat.instMetricSpace`	—	`Metric.isClosedEmbedding_of_pairwise_le_dist` `instDiscreteTopologyInt` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `dist_cast_rat` `pairwise_one_le_dist`
`isUniformEmbedding_coe_rat` 📖	mathematical	—	`IsUniformEmbedding` `instUniformSpaceInt` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `Rat.instMetricSpace`	—	`Metric.isUniformEmbedding_bot_of_pairwise_le_dist` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `dist_cast_rat` `pairwise_one_le_dist`

NNRat

Definitions

Name	Category	Theorems
`instMetricSpace` 📖	CompOp	9 math math: `dist_eq`, `instContinuousSub`, `instContinuousInv₀`, `tendsto_inv_atTop_nhds_zero_nat`, `instContinuousSMulOfIsScalarTowerOfRat`, `nndist_eq`, `instContinuousSMulNNReal`, `instOrderTopology`, `instIsTopologicalSemiring`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dist_eq` 📖	mathematical	—	`Dist.dist` `NNRat` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace` `instMetricSpace` `Rat.instMetricSpace` `cast` `Rat.instNNRatCast`	—	—
`instContinuousInv₀` 📖	mathematical	—	`ContinuousInv₀` `NNRat` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `instSemifield` `instInv` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `instMetricSpace`	—	`IsStrictOrderedRing.toContinuousInv₀` `instIsStrictOrderedRingNNRat` `instOrderTopology` `IsTopologicalSemiring.toContinuousMul` `instIsTopologicalSemiring`
`instContinuousSMulNNReal` 📖	mathematical	—	`ContinuousSMul` `NNRat` `NNReal` `NNReal.instSMulNNRat` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `instMetricSpace` `NNReal.instTopologicalSpace`	—	`Continuous.smul` `instContinuousSMulOfIsScalarTowerOfRat` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `IsScalarTower.nnrat` `Rat.instCharZero` `instContinuousSMulRatReal` `Continuous.fst` `continuous_id'` `Continuous.comp'` `NNReal.continuous_coe` `Continuous.snd`
`instContinuousSMulOfIsScalarTowerOfRat` 📖	mathematical	—	`ContinuousSMul` `NNRat` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `instSemifield` `MulAction.toSemigroupAction` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `instMetricSpace`	—	`Rat.instCharZero` `cast_smul_eq_nnqsmul` `Continuous.smul` `Continuous.comp'` `continuous_induced_dom` `Continuous.fst` `continuous_id'` `Continuous.snd`
`instContinuousSMulRatReal` 📖	mathematical	—	`ContinuousSMul` `Real` `Algebra.toSMul` `Rat.commSemiring` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Real.instDivisionRing` `DivisionRing.toRatAlgebra` `IsStrictOrderedRing.toCharZero` `Ring.toSemiring` `DivisionRing.toRing` `Real.partialOrder` `Real.instIsStrictOrderedRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `Rat.instMetricSpace` `Real.pseudoMetricSpace`	—	`IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `Continuous.smul` `ContinuousMul.to_continuousSMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Continuous.fst'` `continuous_induced_dom` `continuous_snd`
`instContinuousSub` 📖	mathematical	—	`ContinuousSub` `NNRat` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `instMetricSpace` `instSubNNRat`	—	`Continuous.max` `OrderTopology.to_orderClosedTopology` `Rat.instOrderTopology` `Continuous.sub` `IsTopologicalAddGroup.to_continuousSub` `Rat.instIsTopologicalAddGroup` `Continuous.comp'` `continuous_subtype_val` `Continuous.fst` `continuous_id'` `Continuous.snd` `continuous_const`
`instIsTopologicalSemiring` 📖	mathematical	—	`IsTopologicalSemiring` `NNRat` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `instMetricSpace` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `instSemifield`	—	`continuousAdd_induced` `Rat.instIsStrictOrderedRing` `SemilinearMapClass.toAddHomClass` `IsStrictOrderedRing.toCharZero` `Nonneg.isStrictOrderedRing` `Rat.instCharZero` `RingHomClass.toLinearMapClassNNRat` `RingHom.instRingHomClass` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `Rat.instIsTopologicalRing` `continuousMul_induced` `Rat.instZeroLEOneClass` `Rat.instAddLeftMono` `Rat.instPosMulMono` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `IsTopologicalSemiring.toContinuousMul`
`instOrderTopology` 📖	mathematical	—	`OrderTopology` `NNRat` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `instMetricSpace` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderNNRat`	—	`orderTopology_of_ordConnected` `Rat.instOrderTopology` `Set.ordConnected_Ici`
`nndist_eq` 📖	mathematical	—	`NNDist.nndist` `NNRat` `PseudoMetricSpace.toNNDist` `MetricSpace.toPseudoMetricSpace` `instMetricSpace` `Rat.instMetricSpace` `cast` `Rat.instNNRatCast`	—	—

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dist_cast_rat` 📖	mathematical	—	`Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace` `Rat.instMetricSpace` `instDist`	—	`dist_cast_real` `Rat.dist_cast`
`isClosedEmbedding_coe_rat` 📖	mathematical	—	`Topology.IsClosedEmbedding` `instTopologicalSpaceNat` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `Rat.instMetricSpace`	—	`Metric.isClosedEmbedding_of_pairwise_le_dist` `instDiscreteTopologyNat` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `dist_cast_rat` `pairwise_one_le_dist`
`isUniformEmbedding_coe_rat` 📖	mathematical	—	`IsUniformEmbedding` `instUniformSpaceNat` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `Rat.instMetricSpace`	—	`Metric.isUniformEmbedding_bot_of_pairwise_le_dist` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `dist_cast_rat` `pairwise_one_le_dist`

Rat

Definitions

Name	Category	Theorems
`instMetricSpace` 📖	CompOp	33 math math: `continuous_coe_real`, `Int.isUniformEmbedding_coe_rat`, `NNRat.dist_eq`, `Nat.isUniformEmbedding_coe_rat`, `not_countably_generated_cocompact`, `uniformContinuous_neg`, `dist_eq`, `borelSpace`, `dist_cast`, `isDenseEmbedding_coe_real`, `not_firstCountableTopology_opc`, `instOrderTopology`, `cocompact_inf_nhds_neBot`, `Int.dist_cast_rat`, `uniformContinuous_add`, `uniformContinuous_abs`, `Nat.dist_cast_rat`, `Nat.isClosedEmbedding_coe_rat`, `totallyBounded_Icc`, `not_countably_generated_nhds_infty_opc`, `not_secondCountableTopology_opc`, `uniformSpace_eq`, `NNRat.nndist_eq`, `instIsTopologicalRing`, `instIsUniformAddGroup`, `instNoncompactSpace`, `isUniformEmbedding_coe_real`, `isEmbedding_coe_real`, `instIsTopologicalAddGroup`, `instTotallyDisconnectedSpace`, `NNRat.instContinuousSMulRatReal`, `Int.isClosedEmbedding_coe_rat`, `uniformContinuous_coe_real`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_coe_real` 📖	mathematical	—	`Continuous` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `instMetricSpace` `Real.pseudoMetricSpace` `Real.instRatCast`	—	`UniformContinuous.continuous` `uniformContinuous_coe_real`
`dist_cast` 📖	mathematical	—	`Dist.dist` `Real` `PseudoMetricSpace.toDist` `Real.pseudoMetricSpace` `Real.instRatCast` `MetricSpace.toPseudoMetricSpace` `instMetricSpace`	—	—
`dist_eq` 📖	mathematical	—	`Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace` `instMetricSpace` `abs` `Real` `Real.lattice` `Real.instAddGroup` `Real.instSub` `Real.instRatCast`	—	—
`instIsTopologicalAddGroup` 📖	mathematical	—	`IsTopologicalAddGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `instMetricSpace` `addGroup`	—	`IsUniformAddGroup.to_topologicalAddGroup` `instIsUniformAddGroup`
`instIsTopologicalRing` 📖	mathematical	—	`IsTopologicalRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `instMetricSpace` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing`	—	`IsTopologicalDivisionRing.toIsTopologicalRing` `IsStrictOrderedRing.toIsTopologicalDivisionRing` `instIsStrictOrderedRing` `instOrderTopology`
`instIsUniformAddGroup` 📖	mathematical	—	`IsUniformAddGroup` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `instMetricSpace` `addGroup`	—	`IsUniformAddGroup.mk'` `uniformContinuous_add` `uniformContinuous_neg`
`instNoncompactSpace` 📖	mathematical	—	`NoncompactSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `instMetricSpace`	—	`Topology.IsClosedEmbedding.noncompactSpace` `instNoncompactSpaceInt` `Int.isClosedEmbedding_coe_rat`
`instOrderTopology` 📖	mathematical	—	`OrderTopology` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `instMetricSpace` `instPreorder`	—	`induced_orderTopology` `instOrderTopologyReal` `cast_lt` `Real.instIsStrictOrderedRing` `exists_rat_btwn` `Real.instArchimedean`
`isDenseEmbedding_coe_real` 📖	mathematical	—	`IsDenseEmbedding` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `instMetricSpace` `Real.pseudoMetricSpace` `Real.instRatCast`	—	`IsUniformEmbedding.isDenseEmbedding` `isUniformEmbedding_coe_real` `denseRange_cast` `Real.instIsStrictOrderedRing` `instOrderTopologyReal` `Real.instArchimedean`
`isEmbedding_coe_real` 📖	mathematical	—	`Topology.IsEmbedding` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `instMetricSpace` `Real.pseudoMetricSpace` `Real.instRatCast`	—	`IsDenseEmbedding.isEmbedding` `isDenseEmbedding_coe_real`
`isUniformEmbedding_coe_real` 📖	mathematical	—	`IsUniformEmbedding` `Real` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `instMetricSpace` `Real.pseudoMetricSpace` `Real.instRatCast`	—	`isUniformEmbedding_comap` `cast_injective` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing`
`totallyBounded_Icc` 📖	mathematical	—	`TotallyBounded` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `instMetricSpace` `Set.Icc` `instPreorder`	—	`preimage_cast_Icc` `Real.instIsStrictOrderedRing` `totallyBounded_preimage` `IsUniformEmbedding.isUniformInducing` `isUniformEmbedding_coe_real` `totallyBounded_Icc` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `instOrderTopologyReal`
`uniformContinuous_abs` 📖	mathematical	—	`UniformContinuous` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `instMetricSpace` `abs` `instLattice` `addGroup`	—	`Metric.uniformContinuous_iff` `lt_of_le_of_lt` `cast_abs` `Real.instIsStrictOrderedRing` `abs_abs_sub_abs_le_abs_sub` `Real.instIsOrderedAddMonoid`
`uniformContinuous_add` 📖	mathematical	—	`UniformContinuous` `instUniformSpaceProd` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `instMetricSpace`	—	`IsUniformInducing.uniformContinuous_iff` `IsUniformEmbedding.isUniformInducing` `isUniformEmbedding_coe_real` `cast_add` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `UniformContinuous.comp` `Real.uniformContinuous_add` `UniformContinuous.prodMap` `uniformContinuous_coe_real`
`uniformContinuous_coe_real` 📖	mathematical	—	`UniformContinuous` `Real` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `instMetricSpace` `Real.pseudoMetricSpace` `Real.instRatCast`	—	`uniformContinuous_comap`
`uniformContinuous_neg` 📖	mathematical	—	`UniformContinuous` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `instMetricSpace`	—	`Metric.uniformContinuous_iff` `cast_neg` `neg_sub_neg` `abs_sub_comm`

---

← Back to Index