Documentation Verification Report

Lemmas

📁 Source: Mathlib/Topology/MetricSpace/ProperSpace/Lemmas.lean

Statistics

Metric	Count
Definitions	0
Theorems `exists_isLocalMin_mem_ball`, `exists_lt_subset_ball`, `exists_pos_lt_subset_ball`, `isClosedMap_dist`, `isClosedMap_nndist`, `isProperMap_dist`, `isProperMap_nndist`, `properSpace_iff_isProperMap_dist`	8
Total	8

Metric

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_isLocalMin_mem_ball` 📖	mathematical	`ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `closedBall` `Set` `Set.instMembership` `Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	`ball` `IsLocalMin`	—	`IsCompact.exists_isLocalMin_mem_open` `instClosedIicTopology` `OrderTopology.to_orderClosedTopology` `ProperSpace.isCompact_closedBall` `ball_subset_closedBall` `isOpen_ball`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_lt_subset_ball` 📖	mathematical	`Set` `Set.instHasSubset` `Metric.ball`	`Real` `Real.instLT`	—	`le_or_gt` `Set.empty_subset` `NoMinOrder.exists_lt` `instNoMinOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial` `Set.subset_empty_iff` `Metric.ball_eq_empty` `exists_pos_lt_subset_ball`
`exists_pos_lt_subset_ball` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Set` `Set.instHasSubset` `Metric.ball`	`Set.instMembership` `Set.Ioo` `Real.instPreorder`	—	`Set.eq_empty_or_nonempty` `Nat.instAtLeastTwoHAddOfNat` `half_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `half_lt_self` `Set.empty_subset` `IsCompact.of_isClosed_subset` `ProperSpace.isCompact_closedBall` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Metric.ball_subset_closedBall` `IsCompact.exists_isMaxOn` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `instOrderTopologyReal` `Continuous.continuousOn` `Continuous.dist` `continuous_id'` `continuous_const` `exists_between` `LinearOrderedSemiField.toDenselyOrdered` `LE.le.trans_lt` `dist_nonneg` `Metric.closedBall_subset_ball`
`isClosedMap_dist` 📖	mathematical	—	`IsClosedMap` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Dist.dist` `PseudoMetricSpace.toDist`	—	`IsProperMap.isClosedMap` `isProperMap_dist`
`isClosedMap_nndist` 📖	mathematical	—	`IsClosedMap` `NNReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `instPseudoMetricSpaceNNReal` `NNDist.nndist` `PseudoMetricSpace.toNNDist`	—	`IsProperMap.isClosedMap` `isProperMap_nndist`
`isProperMap_dist` 📖	mathematical	—	`IsProperMap` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Dist.dist` `PseudoMetricSpace.toDist`	—	`isProperMap_iff_tendsto_cocompact` `OrderClosedTopology.to_t2Space` `OrderTopology.to_orderClosedTopology` `instOrderTopologyReal` `CompactlyCoherentSpace.of_weaklyLocallyCompactSpace` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `locallyCompact_of_proper` `instProperSpaceReal` `Continuous.dist` `continuous_const` `continuous_id'` `LE.le.trans` `tendsto_dist_left_cocompact_atTop` `atTop_le_cocompact` `instNoMaxOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial` `instClosedIciTopology`
`isProperMap_nndist` 📖	mathematical	—	`IsProperMap` `NNReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `instPseudoMetricSpaceNNReal` `NNDist.nndist` `PseudoMetricSpace.toNNDist`	—	`Continuous.nndist` `continuous_const` `continuous_id'` `continuous_induced_dom` `isProperMap_dist` `NNReal.coe_injective`
`properSpace_iff_isProperMap_dist` 📖	mathematical	—	`ProperSpace` `IsProperMap` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Dist.dist` `PseudoMetricSpace.toDist`	—	`isProperMap_dist` `Set.ext` `dist_comm` `sub_zero` `abs_dist` `IsProperMap.isCompact_preimage` `ProperSpace.isCompact_closedBall` `instProperSpaceReal`

---

← Back to Index