Documentation Verification Report

Int

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

Statistics

Metric	Count
Definitions `instDist`, `instMetricSpace`	2
Theorems `ball_eq_Ioo`, `closedBall_eq_Icc`, `cobounded_eq`, `cofinite_eq`, `dist_cast_real`, `dist_eq`, `dist_eq'`, `instIsOrderBornology`, `instProperSpace`, `isClosedEmbedding_coe_real`, `isUniformEmbedding_coe_real`, `pairwise_one_le_dist`, `preimage_ball`, `preimage_closedBall`	14
Total	16

Int

Definitions

Name	Category	Theorems
`instDist` 📖	CompOp	6 math math: `dist_eq'`, `dist_cast_rat`, `dist_cast_real`, `dist_eq`, `Nat.dist_coe_int`, `pairwise_one_le_dist`
`instMetricSpace` 📖	CompOp	8 math math: `instProperSpace`, `ball_eq_Ioo`, `closedBall_eq_Icc`, `preimage_ball`, `instIsOrderBornology`, `preimage_closedBall`, `Complex.isometry_intCast`, `cobounded_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ball_eq_Ioo` 📖	mathematical	—	`Metric.ball` `MetricSpace.toPseudoMetricSpace` `instMetricSpace` `Set.Ioo` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `floor` `Real` `Real.instRing` `Real.linearOrder` `Real.instFloorRing` `Real.instSub` `Real.instIntCast` `ceil` `Real.instAdd`	—	`preimage_ball` `Real.ball_eq_Ioo` `preimage_Ioo`
`closedBall_eq_Icc` 📖	mathematical	—	`Metric.closedBall` `MetricSpace.toPseudoMetricSpace` `instMetricSpace` `Set.Icc` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `ceil` `Real` `Real.instRing` `Real.linearOrder` `Real.instFloorRing` `Real.instSub` `Real.instIntCast` `floor` `Real.instAdd`	—	`preimage_closedBall` `Real.closedBall_eq_Icc` `preimage_Icc`
`cobounded_eq` 📖	mathematical	—	`Bornology.cobounded` `PseudoMetricSpace.toBornology` `MetricSpace.toPseudoMetricSpace` `instMetricSpace` `Filter` `Filter.instSup` `Filter.atBot` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `Filter.atTop`	—	`Metric.comap_dist_right_atTop` `dist_eq'` `sub_zero` `instIsOrderedAddMonoid` `comap_cast_atTop` `Real.instIsStrictOrderedRing` `Real.instArchimedean` `Filter.comap_comap`
`cofinite_eq` 📖	mathematical	—	`Filter.cofinite` `Filter` `Filter.instSup` `Filter.atBot` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `Filter.atTop`	—	`Filter.cocompact_eq_cofinite` `instDiscreteTopologyInt` `cocompact_eq_atBot_atTop` `instNoMaxOrderOfNontrivial` `IsStrictOrderedRing.toIsOrderedRing` `instIsStrictOrderedRing` `instNontrivial` `instNoMinOrderOfNontrivial` `OrderTopology.to_orderClosedTopology` `OrderTopology.of_linearLocallyFinite` `ConditionallyCompleteLinearOrder.toCompactIccSpace`
`dist_cast_real` 📖	mathematical	—	`Dist.dist` `Real` `PseudoMetricSpace.toDist` `Real.pseudoMetricSpace` `Real.instIntCast` `instDist`	—	—
`dist_eq` 📖	mathematical	—	`Dist.dist` `instDist` `abs` `Real` `Real.lattice` `Real.instAddGroup` `Real.instSub` `Real.instIntCast`	—	—
`dist_eq'` 📖	mathematical	—	`Dist.dist` `instDist` `Real` `Real.instIntCast` `abs` `instLatticeInt` `instAddGroup`	—	`dist_eq` `Real.instIsStrictOrderedRing` `IsStrictOrderedRing.toCharZero`
`instIsOrderBornology` 📖	mathematical	—	`IsOrderBornology` `PseudoMetricSpace.toBornology` `MetricSpace.toPseudoMetricSpace` `instMetricSpace` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder`	—	`IsOrderBornology.of_isCompactIcc` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `OrderTopology.of_linearLocallyFinite` `instDiscreteTopologyInt` `closedBall_eq_Icc` `cast_zero` `zero_sub` `zero_add`
`instProperSpace` 📖	mathematical	—	`ProperSpace` `MetricSpace.toPseudoMetricSpace` `instMetricSpace`	—	`closedBall_eq_Icc` `Set.Finite.isCompact` `Set.finite_Icc`
`isClosedEmbedding_coe_real` 📖	mathematical	—	`Topology.IsClosedEmbedding` `Real` `instTopologicalSpaceInt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instIntCast`	—	`Metric.isClosedEmbedding_of_pairwise_le_dist` `instDiscreteTopologyInt` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `pairwise_one_le_dist`
`isUniformEmbedding_coe_real` 📖	mathematical	—	`IsUniformEmbedding` `Real` `instUniformSpaceInt` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instIntCast`	—	`Metric.isUniformEmbedding_bot_of_pairwise_le_dist` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `pairwise_one_le_dist`
`pairwise_one_le_dist` 📖	mathematical	—	`Pairwise` `Real` `Real.instLE` `Real.instOne` `Dist.dist` `instDist`	—	`dist_eq` `Nat.cast_one` `Real.instIsStrictOrderedRing` `cast_one` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `zero_add` `abs_pos` `instAddLeftMono` `sub_ne_zero`
`preimage_ball` 📖	mathematical	—	`Set.preimage` `Real` `Real.instIntCast` `Metric.ball` `Real.pseudoMetricSpace` `MetricSpace.toPseudoMetricSpace` `instMetricSpace`	—	—
`preimage_closedBall` 📖	mathematical	—	`Set.preimage` `Real` `Real.instIntCast` `Metric.closedBall` `Real.pseudoMetricSpace` `MetricSpace.toPseudoMetricSpace` `instMetricSpace`	—	—

---

← Back to Index