Documentation Verification Report

ProperSpace

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

Statistics

Metric	Count
Definitions `ProperSpace`	1
Theorems `compactSpace`, `isCompact_closedBall`, `of_isClosed`, `of_isCompact_closedBall_of_le`, `of_seq_closedBall`, `complete_of_proper`, `instCompactSpaceElemClosedBallOfProperSpace`, `instProperSpaceAdditive`, `instProperSpaceMultiplicative`, `instProperSpaceOrderDual`, `instProperSpaceReal`, `instSecondCountableTopologyReal`, `isCompact_sphere`, `locallyCompact_of_proper`, `pi_properSpace`, `prod_properSpace`, `proper_of_compact`, `secondCountable_of_proper`	18
Total	19

Metric.sphere

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compactSpace` 📖	mathematical	—	`CompactSpace` `Set.Elem` `Metric.sphere` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace`	—	`isCompact_iff_compactSpace` `isCompact_sphere`

ProperSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCompact_closedBall` 📖	mathematical	—	`IsCompact` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Metric.closedBall`	—	—
`of_isClosed` 📖	mathematical	—	`ProperSpace` `Set.Elem` `Subtype.pseudoMetricSpace` `Set` `Set.instMembership`	—	`Topology.IsEmbedding.isCompact_iff` `Topology.IsEmbedding.subtypeVal` `IsCompact.of_isClosed_subset` `isCompact_closedBall` `IsClosed.isClosedMap_subtype_val` `Metric.isClosed_closedBall` `Set.image_subset_iff` `subset_rfl` `Set.instReflSubset`
`of_isCompact_closedBall_of_le` 📖	mathematical	`IsCompact` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Metric.closedBall`	`ProperSpace`	—	`IsCompact.of_isClosed_subset` `le_max_right` `Metric.isClosed_closedBall` `Metric.closedBall_subset_closedBall` `le_max_left`
`of_seq_closedBall` 📖	mathematical	`Filter.Tendsto` `Real` `Filter.atTop` `Real.instPreorder` `Filter.Eventually` `IsCompact` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Metric.closedBall`	`ProperSpace`	—	`Filter.Eventually.exists` `Filter.Eventually.and` `Filter.Tendsto.eventually_ge_atTop` `IsCompact.of_isClosed_subset` `Metric.isClosed_closedBall` `Metric.closedBall_subset_closedBall'`

(root)

Definitions

Name	Category	Theorems
`ProperSpace` 📖	CompData	30 math math: `Int.instProperSpace`, `FiniteDimensional.proper_rclike`, `LipschitzWith.properSpace`, `ProperSpace.of_seq_closedBall`, `prod_properSpace`, `FiniteDimensional.RCLike.properSpace_submodule`, `instProperSpaceAdditive`, `PNat.instProperSpace`, `ProperSpace.of_nontriviallyNormedField_of_weaklyLocallyCompactSpace`, `PeriodPair.instProperSpaceSubtypeComplexMemSubmoduleIntLattice`, `instProperSpaceReal`, `Valued.integer.properSpace_iff_completeSpace_and_isDiscreteValuationRing_integer_and_finite_residueField`, `instProperSpaceMultiplicative`, `AntilipschitzWith.properSpace`, `Valued.integer.properSpace_iff_compactSpace_integer`, `ProperSpace.of_locallyCompact_module`, `NNReal.instProperSpace`, `ProperSpace.of_locallyCompactSpace`, `Complex.instProperSpace`, `UpperHalfPlane.instProperSpace`, `FiniteDimensional.proper_real`, `FiniteDimensional.proper`, `ProperSpace.of_isClosed`, `ProperSpace.of_isCompact_closedBall_of_le`, `Padic.instProperSpace`, `instProperSpaceOrderDual`, `properSpace_iff_isProperMap_dist`, `proper_of_compact`, `Nat.instProperSpace`, `instProperSpaceSubtypeMemSubmoduleOfCompleteSpaceOfLocallyCompactSpace`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`complete_of_proper` 📖	mathematical	—	`CompleteSpace` `PseudoMetricSpace.toUniformSpace`	—	`Metric.cauchy_iff` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `Filter.NeBot.nonempty_of_mem` `Filter.mem_of_superset` `LT.lt.le` `isCompact_iff_totallyBounded_isComplete` `ProperSpace.isCompact_closedBall` `Filter.le_principal_iff`
`instCompactSpaceElemClosedBallOfProperSpace` 📖	mathematical	—	`CompactSpace` `Set.Elem` `Metric.closedBall` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace`	—	`isCompact_iff_compactSpace` `ProperSpace.isCompact_closedBall`
`instProperSpaceAdditive` 📖	mathematical	—	`ProperSpace` `Additive` `instPseudoMetricSpaceAdditive`	—	—
`instProperSpaceMultiplicative` 📖	mathematical	—	`ProperSpace` `Multiplicative` `instPseudoMetricSpaceMultiplicative`	—	—
`instProperSpaceOrderDual` 📖	mathematical	—	`ProperSpace` `OrderDual` `instPseudoMetricSpaceOrderDual`	—	—
`instProperSpaceReal` 📖	mathematical	—	`ProperSpace` `Real` `Real.pseudoMetricSpace`	—	`ConditionallyCompleteLinearOrder.isCompact_Icc` `instOrderTopologyReal` `Real.closedBall_eq_Icc`
`instSecondCountableTopologyReal` 📖	mathematical	—	`SecondCountableTopology` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	—	`secondCountable_of_proper` `instProperSpaceReal`
`isCompact_sphere` 📖	mathematical	—	`IsCompact` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Metric.sphere`	—	`IsCompact.of_isClosed_subset` `ProperSpace.isCompact_closedBall` `Metric.isClosed_sphere` `Metric.sphere_subset_closedBall`
`locallyCompact_of_proper` 📖	mathematical	—	`LocallyCompactSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace`	—	`LocallyCompactSpace.of_hasBasis` `Metric.nhds_basis_closedBall` `ProperSpace.isCompact_closedBall`
`pi_properSpace` 📖	mathematical	`ProperSpace`	`pseudoMetricSpacePi`	—	`ProperSpace.of_isCompact_closedBall_of_le` `closedBall_pi` `isCompact_univ_pi` `ProperSpace.isCompact_closedBall`
`prod_properSpace` 📖	mathematical	—	`ProperSpace` `Prod.pseudoMetricSpaceMax`	—	`closedBall_prod_same` `IsCompact.prod` `ProperSpace.isCompact_closedBall`
`proper_of_compact` 📖	mathematical	—	`ProperSpace`	—	`IsClosed.isCompact` `Metric.isClosed_closedBall`
`secondCountable_of_proper` 📖	mathematical	—	`SecondCountableTopology` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace`	—	`em` `ProperSpace.isCompact_closedBall` `Metric.iUnion_closedBall_nat` `isCompact_empty` `Set.iUnion_eq_univ_iff` `EMetric.secondCountable_of_sigmaCompact`

---

← Back to Index