Documentation Verification Report

Closeds

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

Statistics

Metric	Count
Definitions `instMetricSpace`, `hausdorff`, `instEMetricSpace`, `instEMetricSpace`, `instEMetricSpace`	5
Theorems `edist_eq`, `isClosed_subsets_of_isClosed`, `isometry_singleton`, `lipschitz_sup`, `isUniformEmbedding`, `continuous_toCloseds`, `isClosed_in_closeds`, `isClosed_subsets_of_isClosed`, `isUniformEmbedding_toCloseds`, `isometry_singleton`, `isometry_toCloseds`, `lipschitz_prod`, `lipschitz_sup`, `continuous_infEdist_hausdorffEdist`, `hausdorffEdist_le_of_mem_hausdorffEntourage`, `isClosed_subsets_of_isClosed`, `mem_hausdorffEntourage_of_hausdorffEdist_lt`, `dist_eq`, `hausdorffEDist_le_of_mem_hausdorffEntourage`, `lipschitz_infDist`, `lipschitz_infDist_set`, `mem_hausdorffEntourage_of_hausdorffEDist_lt`, `uniformContinuous_infDist_Hausdorff_dist`, `continuous_infEDist`, `edist_eq`, `instCompleteSpace`, `isometry_singleton`, `lipschitz_sup`, `edist_eq`, `isometry_singleton`, `isometry_toCloseds`, `lipschitz_prod`, `lipschitz_sup`, `instCompleteSpace`, `instSecondCountableTopology`, `isClosed_in_closeds`, `isometry_singleton`, `isometry_toCloseds`, `isometry_toCompacts`, `lipschitz_prod`, `lipschitz_sup`	41
Total	46

EMetric

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_infEdist_hausdorffEdist` 📖	mathematical	—	`Continuous` `TopologicalSpace.Closeds` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `EMetricSpace.toPseudoEMetricSpace` `ENNReal` `instTopologicalSpaceProd` `TopologicalSpace.Closeds.uniformSpace` `ENNReal.instTopologicalSpace` `Metric.infEDist` `SetLike.coe` `TopologicalSpace.Closeds.instSetLike`	—	`TopologicalSpace.Closeds.continuous_infEDist`
`hausdorffEdist_le_of_mem_hausdorffEntourage` 📖	mathematical	`Set` `SetRel` `Set.instMembership` `hausdorffEntourage` `setOf` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `EDist.edist` `PseudoEMetricSpace.toEDist`	`Metric.hausdorffEDist`	—	`Metric.hausdorffEDist_le_of_mem_hausdorffEntourage`
`isClosed_subsets_of_isClosed` 📖	mathematical	—	`IsClosed` `TopologicalSpace.Closeds` `UniformSpace.toTopologicalSpace` `TopologicalSpace.Closeds.uniformSpace` `setOf` `Set` `Set.instHasSubset` `SetLike.coe` `TopologicalSpace.Closeds.instSetLike`	—	`TopologicalSpace.Closeds.isClosed_subsets_of_isClosed`
`mem_hausdorffEntourage_of_hausdorffEdist_lt` 📖	mathematical	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Metric.hausdorffEDist`	`Set` `SetRel` `Set.instMembership` `hausdorffEntourage` `setOf` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	`Metric.mem_hausdorffEntourage_of_hausdorffEDist_lt`

EMetric.Closeds

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`edist_eq` 📖	mathematical	—	`EDist.edist` `TopologicalSpace.Closeds` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `EMetricSpace.toPseudoEMetricSpace` `PseudoEMetricSpace.toEDist` `TopologicalSpace.Closeds.instEMetricSpace` `Metric.hausdorffEDist` `SetLike.coe` `TopologicalSpace.Closeds.instSetLike`	—	`TopologicalSpace.Closeds.edist_eq`
`isClosed_subsets_of_isClosed` 📖	mathematical	—	`IsClosed` `TopologicalSpace.Closeds` `UniformSpace.toTopologicalSpace` `TopologicalSpace.Closeds.uniformSpace` `setOf` `Set` `Set.instHasSubset` `SetLike.coe` `TopologicalSpace.Closeds.instSetLike`	—	`TopologicalSpace.Closeds.isClosed_subsets_of_isClosed`
`isometry_singleton` 📖	mathematical	—	`Isometry` `TopologicalSpace.Closeds` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `EMetricSpace.toPseudoEMetricSpace` `TopologicalSpace.Closeds.instEMetricSpace` `TopologicalSpace.Closeds.instSingletonOfT1Space` `T2Space.t1Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace`	—	`TopologicalSpace.Closeds.isometry_singleton`
`lipschitz_sup` 📖	mathematical	—	`LipschitzWith` `TopologicalSpace.Closeds` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `EMetricSpace.toPseudoEMetricSpace` `Prod.pseudoEMetricSpaceMax` `TopologicalSpace.Closeds.instEMetricSpace` `NNReal` `instOneNNReal` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.Closeds.instCompleteLattice`	—	`TopologicalSpace.Closeds.lipschitz_sup`

EMetric.NonemptyCompacts

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_toCloseds` 📖	mathematical	—	`Continuous` `TopologicalSpace.NonemptyCompacts` `UniformSpace.toTopologicalSpace` `TopologicalSpace.Closeds` `TopologicalSpace.NonemptyCompacts.topology` `TopologicalSpace.Closeds.uniformSpace` `TopologicalSpace.NonemptyCompacts.toCloseds`	—	`TopologicalSpace.NonemptyCompacts.continuous_toCloseds`
`isClosed_in_closeds` 📖	mathematical	—	`IsClosed` `TopologicalSpace.Closeds` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `EMetricSpace.toPseudoEMetricSpace` `TopologicalSpace.Closeds.uniformSpace` `Set.range` `TopologicalSpace.NonemptyCompacts` `TopologicalSpace.NonemptyCompacts.toCloseds` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace`	—	`TopologicalSpace.NonemptyCompacts.isClosed_in_closeds`
`isClosed_subsets_of_isClosed` 📖	mathematical	—	`IsClosed` `TopologicalSpace.NonemptyCompacts` `TopologicalSpace.NonemptyCompacts.topology` `setOf` `Set` `Set.instHasSubset` `SetLike.coe` `TopologicalSpace.NonemptyCompacts.instSetLike`	—	`TopologicalSpace.NonemptyCompacts.isClosed_subsets_of_isClosed`
`isUniformEmbedding_toCloseds` 📖	mathematical	—	`IsUniformEmbedding` `TopologicalSpace.NonemptyCompacts` `UniformSpace.toTopologicalSpace` `TopologicalSpace.Closeds` `TopologicalSpace.NonemptyCompacts.uniformSpace` `TopologicalSpace.Closeds.uniformSpace` `TopologicalSpace.NonemptyCompacts.toCloseds`	—	`TopologicalSpace.NonemptyCompacts.isUniformEmbedding_toCloseds`
`isometry_singleton` 📖	mathematical	—	`Isometry` `TopologicalSpace.NonemptyCompacts` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `EMetricSpace.toPseudoEMetricSpace` `TopologicalSpace.NonemptyCompacts.instEMetricSpace` `TopologicalSpace.NonemptyCompacts.instSingleton`	—	`TopologicalSpace.NonemptyCompacts.isometry_singleton`
`isometry_toCloseds` 📖	mathematical	—	`Isometry` `TopologicalSpace.NonemptyCompacts` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `EMetricSpace.toPseudoEMetricSpace` `TopologicalSpace.Closeds` `TopologicalSpace.NonemptyCompacts.instEMetricSpace` `TopologicalSpace.Closeds.instEMetricSpace` `TopologicalSpace.NonemptyCompacts.toCloseds` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace`	—	`TopologicalSpace.NonemptyCompacts.isometry_toCloseds`
`lipschitz_prod` 📖	mathematical	—	`LipschitzWith` `TopologicalSpace.NonemptyCompacts` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `EMetricSpace.toPseudoEMetricSpace` `instTopologicalSpaceProd` `Prod.pseudoEMetricSpaceMax` `TopologicalSpace.NonemptyCompacts.instEMetricSpace` `Prod.emetricSpaceMax` `NNReal` `instOneNNReal` `SProd.sprod` `TopologicalSpace.NonemptyCompacts.instSProdProd`	—	`TopologicalSpace.NonemptyCompacts.lipschitz_prod`
`lipschitz_sup` 📖	mathematical	—	`LipschitzWith` `TopologicalSpace.NonemptyCompacts` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `EMetricSpace.toPseudoEMetricSpace` `Prod.pseudoEMetricSpaceMax` `TopologicalSpace.NonemptyCompacts.instEMetricSpace` `NNReal` `instOneNNReal` `TopologicalSpace.NonemptyCompacts.instMax`	—	`TopologicalSpace.NonemptyCompacts.lipschitz_sup`

EMetric.NonemptyCompacts.ToCloseds

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isUniformEmbedding` 📖	mathematical	—	`IsUniformEmbedding` `TopologicalSpace.NonemptyCompacts` `UniformSpace.toTopologicalSpace` `TopologicalSpace.Closeds` `TopologicalSpace.NonemptyCompacts.uniformSpace` `TopologicalSpace.Closeds.uniformSpace` `TopologicalSpace.NonemptyCompacts.toCloseds`	—	`TopologicalSpace.NonemptyCompacts.isUniformEmbedding_toCloseds`

Metric

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hausdorffEDist_le_of_mem_hausdorffEntourage` 📖	mathematical	`Set` `SetRel` `Set.instMembership` `hausdorffEntourage` `setOf` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `EDist.edist` `PseudoEMetricSpace.toEDist`	`hausdorffEDist`	—	`hausdorffEDist_def` `max_le_iff` `iSup₂_le_iff` `iInf₂_le_of_le` `PseudoEMetricSpace.edist_comm` `Set.mem_setOf` `hausdorffEntourage.eq_1`
`lipschitz_infDist` 📖	mathematical	—	`LipschitzWith` `TopologicalSpace.NonemptyCompacts` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `Real` `Prod.pseudoEMetricSpaceMax` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `TopologicalSpace.NonemptyCompacts.instEMetricSpace` `Real.metricSpace` `NNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `Nat.instAtLeastTwoHAddOfNat` `infDist` `SetLike.coe` `TopologicalSpace.NonemptyCompacts.instSetLike`	—	`Nat.instAtLeastTwoHAddOfNat` `one_add_one_eq_two` `LipschitzWith.uncurry` `lipschitz_infDist_pt` `lipschitz_infDist_set`
`lipschitz_infDist_set` 📖	mathematical	—	`LipschitzWith` `TopologicalSpace.NonemptyCompacts` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `Real` `EMetricSpace.toPseudoEMetricSpace` `TopologicalSpace.NonemptyCompacts.instEMetricSpace` `MetricSpace.toEMetricSpace` `Real.metricSpace` `NNReal` `instOneNNReal` `infDist` `SetLike.coe` `TopologicalSpace.NonemptyCompacts.instSetLike`	—	`LipschitzWith.of_le_add` `dist_comm` `infDist_le_infDist_add_hausdorffDist` `edist_ne_top`
`mem_hausdorffEntourage_of_hausdorffEDist_lt` 📖	mathematical	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `hausdorffEDist`	`Set` `SetRel` `Set.instMembership` `hausdorffEntourage` `setOf` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	`hausdorffEntourage.eq_1` `Set.mem_setOf` `PseudoEMetricSpace.edist_comm` `LE.le.trans_lt` `le_iSup₂` `max_lt_iff` `hausdorffEDist_def`
`uniformContinuous_infDist_Hausdorff_dist` 📖	mathematical	—	`UniformContinuous` `TopologicalSpace.NonemptyCompacts` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `Real` `instUniformSpaceProd` `TopologicalSpace.NonemptyCompacts.uniformSpace` `Real.pseudoMetricSpace` `infDist` `SetLike.coe` `TopologicalSpace.NonemptyCompacts.instSetLike`	—	`LipschitzWith.uniformContinuous` `Nat.instAtLeastTwoHAddOfNat` `lipschitz_infDist`

Metric.NonemptyCompacts

Definitions

Name	Category	Theorems
`instMetricSpace` 📖	CompOp	2 math math: `GromovHausdorff.ghDist_le_nonemptyCompacts_dist`, `dist_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dist_eq` 📖	mathematical	—	`Dist.dist` `TopologicalSpace.NonemptyCompacts` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `PseudoMetricSpace.toDist` `instMetricSpace` `Metric.hausdorffDist` `SetLike.coe` `TopologicalSpace.NonemptyCompacts.instSetLike`	—	—

PseudoEMetricSpace

Definitions

Name	Category	Theorems
`hausdorff` 📖	CompOp	—

TopologicalSpace.Closeds

Definitions

Name	Category	Theorems
`instEMetricSpace` 📖	CompOp	9 math math: `EMetric.NonemptyCompacts.isometry_toCloseds`, `EMetric.Closeds.isometry_singleton`, `lipschitz_sup`, `edist_eq`, `isometry_singleton`, `TopologicalSpace.NonemptyCompacts.isometry_toCloseds`, `EMetric.Closeds.lipschitz_sup`, `EMetric.Closeds.edist_eq`, `TopologicalSpace.Compacts.isometry_toCloseds`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_infEDist` 📖	mathematical	—	`Continuous` `TopologicalSpace.Closeds` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `EMetricSpace.toPseudoEMetricSpace` `ENNReal` `instTopologicalSpaceProd` `uniformSpace` `ENNReal.instTopologicalSpace` `Metric.infEDist` `SetLike.coe` `instSetLike`	—	`continuous_of_le_add_edist` `Nat.instAtLeastTwoHAddOfNat` `Metric.infEDist_le_infEDist_add_hausdorffEDist` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `Metric.infEDist_le_infEDist_add_edist` `add_assoc` `Metric.hausdorffEDist_comm` `add_le_add_right` `add_le_add` `le_max_left` `le_max_right` `mul_two` `mul_comm`
`edist_eq` 📖	mathematical	—	`EDist.edist` `TopologicalSpace.Closeds` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `EMetricSpace.toPseudoEMetricSpace` `PseudoEMetricSpace.toEDist` `instEMetricSpace` `Metric.hausdorffEDist` `SetLike.coe` `instSetLike`	—	—
`instCompleteSpace` 📖	mathematical	—	`CompleteSpace` `TopologicalSpace.Closeds` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `EMetricSpace.toPseudoEMetricSpace` `uniformSpace`	—	`Nat.instAtLeastTwoHAddOfNat` `ENNReal.pow_ne_top` `ENNReal.Finiteness.inv_ne_top` `ne_of_gt` `Mathlib.Meta.Positivity.pos_of_isNat` `ENNReal.instIsOrderedRing` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `EMetric.complete_of_convergent_controlled_sequences` `isClosed_iInter` `isClosed_closure` `Metric.exists_edist_lt_of_hausdorffEDist_lt` `div_eq_mul_inv` `ENNReal.inv_pow` `pow_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `Nat.instCanonicallyOrderedAdd` `le_of_lt` `cauchySeq_of_edist_le_geometric_two` `cauchySeq_tendsto_of_complete` `Set.mem_iInter` `mem_closure_of_tendsto` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `edist_le_of_edist_le_geometric_two_of_tendsto₀` `EMetric.mem_closure_iff` `le_refl` `PseudoEMetricSpace.edist_triangle` `add_le_add` `ENNReal.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `two_mul` `Metric.hausdorffEDist_le_of_mem_edist` `EMetric.tendsto_atTop` `ENNReal.Tendsto.const_mul` `ENNReal.tendsto_pow_atTop_nhds_zero_of_lt_one` `IsOrderedRing.toZeroLEOneClass` `ENNReal.instCharZero` `Filter.Eventually.exists_forall_of_atTop` `tendsto_order` `ENNReal.instOrderTopology` `MulZeroClass.mul_zero` `lt_of_le_of_lt`
`isometry_singleton` 📖	mathematical	—	`Isometry` `TopologicalSpace.Closeds` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `EMetricSpace.toPseudoEMetricSpace` `instEMetricSpace` `instSingletonOfT1Space` `T2Space.t1Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace`	—	`Metric.hausdorffEDist_singleton`
`lipschitz_sup` 📖	mathematical	—	`LipschitzWith` `TopologicalSpace.Closeds` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `EMetricSpace.toPseudoEMetricSpace` `Prod.pseudoEMetricSpaceMax` `instEMetricSpace` `NNReal` `instOneNNReal` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice`	—	`LipschitzWith.of_edist_le` `Metric.hausdorffEDist_union_le`

TopologicalSpace.Compacts

Definitions

Name	Category	Theorems
`instEMetricSpace` 📖	CompOp	6 math math: `lipschitz_prod`, `edist_eq`, `lipschitz_sup`, `isometry_singleton`, `isometry_toCloseds`, `TopologicalSpace.NonemptyCompacts.isometry_toCompacts`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`edist_eq` 📖	mathematical	—	`EDist.edist` `TopologicalSpace.Compacts` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `EMetricSpace.toPseudoEMetricSpace` `PseudoEMetricSpace.toEDist` `instEMetricSpace` `Metric.hausdorffEDist` `SetLike.coe` `instSetLike`	—	—
`isometry_singleton` 📖	mathematical	—	`Isometry` `TopologicalSpace.Compacts` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `EMetricSpace.toPseudoEMetricSpace` `instEMetricSpace` `instSingleton`	—	`Metric.hausdorffEDist_singleton`
`isometry_toCloseds` 📖	mathematical	—	`Isometry` `TopologicalSpace.Compacts` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `EMetricSpace.toPseudoEMetricSpace` `TopologicalSpace.Closeds` `instEMetricSpace` `TopologicalSpace.Closeds.instEMetricSpace` `toCloseds` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace`	—	`TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace`
`lipschitz_prod` 📖	mathematical	—	`LipschitzWith` `TopologicalSpace.Compacts` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `EMetricSpace.toPseudoEMetricSpace` `instTopologicalSpaceProd` `Prod.pseudoEMetricSpaceMax` `instEMetricSpace` `Prod.emetricSpaceMax` `NNReal` `instOneNNReal` `SProd.sprod` `instSProdProd`	—	`LipschitzWith.of_edist_le` `Metric.hausdorffEDist_prod_le`
`lipschitz_sup` 📖	mathematical	—	`LipschitzWith` `TopologicalSpace.Compacts` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `EMetricSpace.toPseudoEMetricSpace` `Prod.pseudoEMetricSpaceMax` `instEMetricSpace` `NNReal` `instOneNNReal` `instMax`	—	`LipschitzWith.of_edist_le` `Metric.hausdorffEDist_union_le`

TopologicalSpace.NonemptyCompacts

Definitions

Name	Category	Theorems
`instEMetricSpace` 📖	CompOp	12 math math: `EMetric.NonemptyCompacts.lipschitz_prod`, `EMetric.NonemptyCompacts.isometry_toCloseds`, `isometry_singleton`, `lipschitz_prod`, `isometry_toCloseds`, `lipschitz_sup`, `GromovHausdorff.toGHSpace_lipschitz`, `Metric.lipschitz_infDist`, `EMetric.NonemptyCompacts.isometry_singleton`, `Metric.lipschitz_infDist_set`, `EMetric.NonemptyCompacts.lipschitz_sup`, `isometry_toCompacts`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instCompleteSpace` 📖	mathematical	—	`CompleteSpace` `TopologicalSpace.NonemptyCompacts` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `EMetricSpace.toPseudoEMetricSpace` `uniformSpace`	—	`TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `completeSpace_iff_isComplete_range` `Isometry.isUniformInducing` `isometry_toCloseds` `IsClosed.isComplete` `TopologicalSpace.Closeds.instCompleteSpace` `isClosed_in_closeds`
`instSecondCountableTopology` 📖	mathematical	—	`SecondCountableTopology` `TopologicalSpace.NonemptyCompacts` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `EMetricSpace.toPseudoEMetricSpace` `topology`	—	`UniformSpace.secondCountable_of_separable` `EMetric.instIsCountablyGeneratedUniformity` `TopologicalSpace.exists_countable_dense` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `Set.countable_setOf_finite_subset` `Set.Countable.preimage` `SetLike.coe_injective` `EMetric.mem_closure_iff` `exists_between` `ENNReal.instDenselyOrdered` `Nat.instAtLeastTwoHAddOfNat` `ENNReal.half_pos` `LT.lt.ne'` `IsCompact.totallyBounded` `isCompact` `EMetric.totallyBounded_iff` `Set.Finite.image` `Set.mem_iUnion₂` `Set.mem_image_of_mem` `PseudoEMetricSpace.edist_triangle` `ENNReal.add_lt_add` `ENNReal.add_halves` `Set.Finite.subset` `le_of_lt` `PseudoEMetricSpace.edist_comm` `Metric.hausdorffEDist_le_of_mem_edist` `LE.le.trans_lt` `Metric.nonempty_of_hausdorffEDist_ne_top` `nonempty` `ne_top_of_lt` `Set.Finite.isCompact` `Set.mem_image`
`isClosed_in_closeds` 📖	mathematical	—	`IsClosed` `TopologicalSpace.Closeds` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `EMetricSpace.toPseudoEMetricSpace` `TopologicalSpace.Closeds.uniformSpace` `Set.range` `TopologicalSpace.NonemptyCompacts` `toCloseds` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace`	—	`TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Set.ext` `nonempty` `isCompact` `TopologicalSpace.Closeds.ext` `isClosed_of_closure_subset` `EMetric.mem_closure_iff` `ENNReal.coe_lt_top` `Metric.nonempty_of_hausdorffEDist_ne_top` `ne_of_lt` `PseudoEMetricSpace.edist_comm` `isCompact_iff_totallyBounded_isComplete` `EMetric.totallyBounded_iff` `Nat.instAtLeastTwoHAddOfNat` `ENNReal.half_pos` `LT.lt.ne'` `Metric.exists_edist_lt_of_hausdorffEDist_lt` `Set.mem_iUnion₂` `PseudoEMetricSpace.edist_triangle` `ENNReal.add_lt_add` `ENNReal.add_halves` `Set.mem_biUnion` `IsClosed.isComplete` `TopologicalSpace.Closeds.isClosed`
`isometry_singleton` 📖	mathematical	—	`Isometry` `TopologicalSpace.NonemptyCompacts` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `EMetricSpace.toPseudoEMetricSpace` `instEMetricSpace` `instSingleton`	—	`Metric.hausdorffEDist_singleton`
`isometry_toCloseds` 📖	mathematical	—	`Isometry` `TopologicalSpace.NonemptyCompacts` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `EMetricSpace.toPseudoEMetricSpace` `TopologicalSpace.Closeds` `instEMetricSpace` `TopologicalSpace.Closeds.instEMetricSpace` `toCloseds` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace`	—	`TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace`
`isometry_toCompacts` 📖	mathematical	—	`Isometry` `TopologicalSpace.NonemptyCompacts` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `EMetricSpace.toPseudoEMetricSpace` `TopologicalSpace.Compacts` `instEMetricSpace` `TopologicalSpace.Compacts.instEMetricSpace` `toCompacts`	—	—
`lipschitz_prod` 📖	mathematical	—	`LipschitzWith` `TopologicalSpace.NonemptyCompacts` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `EMetricSpace.toPseudoEMetricSpace` `instTopologicalSpaceProd` `Prod.pseudoEMetricSpaceMax` `instEMetricSpace` `Prod.emetricSpaceMax` `NNReal` `instOneNNReal` `SProd.sprod` `instSProdProd`	—	`LipschitzWith.of_edist_le` `Metric.hausdorffEDist_prod_le`
`lipschitz_sup` 📖	mathematical	—	`LipschitzWith` `TopologicalSpace.NonemptyCompacts` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `EMetricSpace.toPseudoEMetricSpace` `Prod.pseudoEMetricSpaceMax` `instEMetricSpace` `NNReal` `instOneNNReal` `instMax`	—	`LipschitzWith.of_edist_le` `Metric.hausdorffEDist_union_le`

---

← Back to Index