Documentation Verification Report

Basic

📁 Source: Mathlib/Topology/MetricSpace/Pseudo/Basic.lean

Statistics

Metric	Count
Definitions	0
Theorems `isSeparable_image`, `dist_eq_zero`, `nndist_eq_zero`, `finite_cover_balls`, `isSeparable`, `cauchy_iff`, `controlled_of_isUniformEmbedding`, `exists_ball_inter_eq_singleton_of_mem_discrete`, `exists_closedBall_inter_eq_singleton_of_discrete`, `finite_approx_of_totallyBounded`, `inseparable_iff`, `inseparable_iff_nndist`, `isUniformEmbedding_iff`, `isUniformInducing_iff`, `secondCountable_of_almost_dense_set`, `tendstoLocallyUniformlyOn_iff`, `tendstoLocallyUniformly_iff`, `tendstoUniformlyOnFilter_iff`, `tendstoUniformlyOn_iff`, `tendstoUniformly_iff`, `totallyBounded_iff`, `totallyBounded_of_finite_discretization`, `isSeparable_preimage`, `isSeparable_preimage`, `cauchySeq_iff_tendsto_dist_atTop_0`, `dist_le_Ico_sum_dist`, `dist_le_Ico_sum_of_dist_le`, `dist_le_range_sum_dist`, `dist_le_range_sum_of_dist_le`, `exists_finite_cover_balls_of_isCompact_closure`, `finite_cover_balls_of_compact`, `tendsto_nhds_unique_dist`	32
Total	32

ContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSeparable_image` 📖	mathematical	`ContinuousOn` `TopologicalSpace.IsSeparable`	`Set.image`	—	`Set.image_eq_range` `Set.image_univ` `TopologicalSpace.IsSeparable.image` `TopologicalSpace.isSeparable_univ_iff` `TopologicalSpace.IsSeparable.separableSpace` `restrict`

Inseparable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dist_eq_zero` 📖	mathematical	`Inseparable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace`	`Dist.dist` `PseudoMetricSpace.toDist` `Real` `Real.instZero`	—	`Metric.inseparable_iff`
`nndist_eq_zero` 📖	mathematical	`Inseparable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace`	`NNDist.nndist` `PseudoMetricSpace.toNNDist` `NNReal` `instZeroNNReal`	—	`Metric.inseparable_iff_nndist`

IsCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_cover_balls` 📖	mathematical	`IsCompact` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real` `Real.instLT` `Real.instZero`	`Set` `Set.instHasSubset` `Set.Finite` `Set.iUnion` `Set.instMembership` `Metric.ball`	—	`finite_cover_balls_of_compact`
`isSeparable` 📖	mathematical	`IsCompact`	`TopologicalSpace.IsSeparable`	—	`TopologicalSpace.IsSeparable.of_subtype` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace` `instLindelofSpaceOfSigmaCompactSpace` `CompactSpace.sigmaCompact` `isCompact_iff_compactSpace` `TopologicalSpace.PseudoMetrizableSpace.subtype`

Metric

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cauchy_iff` 📖	mathematical	—	`Cauchy` `PseudoMetricSpace.toUniformSpace` `Filter.NeBot` `Set` `Filter` `Filter.instMembership` `Real` `Real.instLT` `Dist.dist` `PseudoMetricSpace.toDist`	—	`Filter.HasBasis.cauchy_iff` `uniformity_basis_dist`
`controlled_of_isUniformEmbedding` 📖	mathematical	`IsUniformEmbedding` `PseudoMetricSpace.toUniformSpace`	`Real` `Real.instLT` `Real.instZero` `Dist.dist` `PseudoMetricSpace.toDist`	—	`uniformContinuous_iff` `IsUniformInducing.uniformContinuous` `IsUniformEmbedding.toIsUniformInducing` `isUniformEmbedding_iff`
`exists_ball_inter_eq_singleton_of_mem_discrete` 📖	mathematical	`IsDiscrete` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Set` `Set.instMembership`	`Real` `Real.instLT` `Real.instZero` `Set.instInter` `ball` `Set.instSingletonSet`	—	`Filter.HasBasis.exists_inter_eq_singleton_of_mem_discrete` `nhds_basis_ball`
`exists_closedBall_inter_eq_singleton_of_discrete` 📖	mathematical	`IsDiscrete` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Set` `Set.instMembership`	`Real` `Real.instLT` `Real.instZero` `Set.instInter` `closedBall` `Set.instSingletonSet`	—	`Filter.HasBasis.exists_inter_eq_singleton_of_mem_discrete` `nhds_basis_closedBall`
`finite_approx_of_totallyBounded` 📖	mathematical	`TotallyBounded` `PseudoMetricSpace.toUniformSpace` `Real` `Real.instLT` `Real.instZero`	`Set` `Set.instHasSubset` `Set.Finite` `Set.iUnion` `Set.instMembership` `ball`	—	`totallyBounded_iff_subset` `dist_mem_uniformity`
`inseparable_iff` 📖	mathematical	—	`Inseparable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Dist.dist` `PseudoMetricSpace.toDist` `Real` `Real.instZero`	—	`inseparable_iff_nndist` `dist_nndist` `NNReal.coe_eq_zero`
`inseparable_iff_nndist` 📖	mathematical	—	`Inseparable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `NNDist.nndist` `PseudoMetricSpace.toNNDist` `NNReal` `instZeroNNReal`	—	`EMetric.inseparable_iff` `edist_nndist` `ENNReal.coe_eq_zero`
`isUniformEmbedding_iff` 📖	mathematical	—	`IsUniformEmbedding` `PseudoMetricSpace.toUniformSpace` `UniformContinuous` `Real` `Real.instLT` `Real.instZero` `Dist.dist` `PseudoMetricSpace.toDist`	—	`isUniformEmbedding_iff` `isUniformInducing_iff`
`isUniformInducing_iff` 📖	mathematical	—	`IsUniformInducing` `PseudoMetricSpace.toUniformSpace` `UniformContinuous` `Real` `Real.instLT` `Real.instZero` `Dist.dist` `PseudoMetricSpace.toDist`	—	`isUniformInducing_iff'` `Iff.and` `Filter.HasBasis.le_basis_iff` `Filter.HasBasis.comap` `uniformity_basis_dist`
`secondCountable_of_almost_dense_set` 📖	mathematical	`Set.Countable` `Set` `Set.instMembership` `Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist`	`SecondCountableTopology` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace`	—	`EMetric.secondCountable_of_almost_dense_set` `ENNReal.lt_iff_exists_nnreal_btwn` `Set.iUnion₂_eq_univ_iff` `le_trans` `LT.lt.le` `Nat.cast_zero`
`tendstoLocallyUniformlyOn_iff` 📖	mathematical	—	`TendstoLocallyUniformlyOn` `PseudoMetricSpace.toUniformSpace` `Set` `Filter` `Filter.instMembership` `nhdsWithin` `Filter.Eventually`	—	`dist_mem_uniformity` `mem_uniformity_dist` `Filter.Eventually.mono`
`tendstoLocallyUniformly_iff` 📖	mathematical	—	`TendstoLocallyUniformly` `PseudoMetricSpace.toUniformSpace` `Set` `Filter` `Filter.instMembership` `nhds` `Filter.Eventually`	—	`nhdsWithin_univ`
`tendstoUniformlyOnFilter_iff` 📖	mathematical	—	`TendstoUniformlyOnFilter` `PseudoMetricSpace.toUniformSpace` `Filter.Eventually` `Real` `Real.instLT` `Dist.dist` `PseudoMetricSpace.toDist` `SProd.sprod` `Filter` `Filter.instSProd`	—	`dist_mem_uniformity` `mem_uniformity_dist` `Filter.Eventually.mono`
`tendstoUniformlyOn_iff` 📖	mathematical	—	`TendstoUniformlyOn` `PseudoMetricSpace.toUniformSpace` `Filter.Eventually`	—	`dist_mem_uniformity` `mem_uniformity_dist` `Filter.Eventually.mono`
`tendstoUniformly_iff` 📖	mathematical	—	`TendstoUniformly` `PseudoMetricSpace.toUniformSpace` `Filter.Eventually`	—	`tendstoUniformlyOn_univ` `tendstoUniformlyOn_iff`
`totallyBounded_iff` 📖	mathematical	—	`TotallyBounded` `PseudoMetricSpace.toUniformSpace` `Set.Finite` `Set` `Set.instHasSubset` `Set.iUnion` `Set.instMembership` `ball`	—	`Filter.HasBasis.totallyBounded_iff` `uniformity_basis_dist`
`totallyBounded_of_finite_discretization` 📖	mathematical	`Real` `Real.instLT` `Dist.dist` `PseudoMetricSpace.toDist` `Set` `Set.instMembership`	`TotallyBounded` `PseudoMetricSpace.toUniformSpace`	—	`Set.eq_empty_or_nonempty` `totallyBounded_empty` `totallyBounded_iff` `Set.finite_range` `Finite.of_fintype` `Function.invFun_eq` `Set.iUnion_congr_Prop`

Topology.IsEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSeparable_preimage` 📖	mathematical	`Topology.IsEmbedding` `TopologicalSpace.IsSeparable`	`Set.preimage`	—	`Topology.IsInducing.isSeparable_preimage` `isInducing`

Topology.IsInducing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSeparable_preimage` 📖	mathematical	`Topology.IsInducing` `TopologicalSpace.IsSeparable`	`Set.preimage`	—	`TopologicalSpace.pseudoMetrizableSpaceUniformity_countably_generated` `TopologicalSpace.IsSeparable.separableSpace` `UniformSpace.secondCountable_of_separable` `instIsCountablyGeneratedProdElemUniformity` `Set.mapsTo_preimage` `codRestrict` `comp` `subtypeVal` `secondCountableTopology` `TopologicalSpace.IsSeparable.of_subtype` `TopologicalSpace.SecondCountableTopology.to_separableSpace`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cauchySeq_iff_tendsto_dist_atTop_0` 📖	mathematical	—	`CauchySeq` `PseudoMetricSpace.toUniformSpace` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Filter.Tendsto` `Real` `Dist.dist` `PseudoMetricSpace.toDist` `Filter.atTop` `Prod.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `Real.pseudoMetricSpace` `Real.instZero`	—	`cauchySeq_iff_tendsto` `Metric.uniformity_eq_comap_nhds_zero` `Filter.tendsto_comap_iff`
`dist_le_Ico_sum_dist` 📖	mathematical	—	`Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `Finset.sum` `Real.instAddCommMonoid` `Finset.Ico` `Nat.instPreorder` `Nat.instLocallyFiniteOrder`	—	`Nat.le_induction` `Finset.Ico_self` `Finset.sum_empty` `dist_self` `le_refl` `dist_triangle` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `le_rfl` `Finset.insert_Ico_right_eq_Ico_add_one` `Nat.instNoMaxOrder` `Finset.sum_insert` `add_comm`
`dist_le_Ico_sum_of_dist_le` 📖	mathematical	`Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist`	`Finset.sum` `Real.instAddCommMonoid` `Finset.Ico` `Nat.instPreorder` `Nat.instLocallyFiniteOrder`	—	`le_trans` `dist_le_Ico_sum_dist` `Finset.sum_le_sum` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Finset.mem_Ico`
`dist_le_range_sum_dist` 📖	mathematical	—	`Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `Finset.sum` `Real.instAddCommMonoid` `Finset.range`	—	`dist_le_Ico_sum_dist` `Nat.Ico_zero_eq_range`
`dist_le_range_sum_of_dist_le` 📖	mathematical	`Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist`	`Finset.sum` `Real.instAddCommMonoid` `Finset.range`	—	`dist_le_Ico_sum_of_dist_le` `zero_le` `Nat.instCanonicallyOrderedAdd` `Nat.Ico_zero_eq_range`
`exists_finite_cover_balls_of_isCompact_closure` 📖	mathematical	`IsCompact` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `closure` `Real` `Real.instLT` `Real.instZero`	`Set` `Set.instHasSubset` `Set.Finite` `Set.iUnion` `Set.instMembership` `Metric.ball`	—	`IsCompact.elim_finite_subcover` `Metric.isOpen_ball` `Metric.mem_closure_iff` `Set.mem_iUnion` `Subtype.val_injective` `Finset.coe_map` `Set.image_congr` `Subtype.coe_preimage_self` `Finset.finite_toSet` `Set.iUnion_congr_Prop` `Set.iUnion_exists` `Set.iUnion_coe_set` `HasSubset.Subset.trans` `Set.instIsTransSubset` `subset_closure`
`finite_cover_balls_of_compact` 📖	mathematical	`IsCompact` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real` `Real.instLT` `Real.instZero`	`Set` `Set.instHasSubset` `Set.Finite` `Set.iUnion` `Set.instMembership` `Metric.ball`	—	`IsCompact.elim_nhds_subcover` `Metric.ball_mem_nhds` `Finset.finite_toSet`
`tendsto_nhds_unique_dist` 📖	mathematical	`Filter.Tendsto` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace`	`Dist.dist` `PseudoMetricSpace.toDist` `Real` `Real.instZero`	—	`Inseparable.dist_eq_zero` `tendsto_nhds_unique_inseparable` `instR1Space` `TopologicalSpace.PseudoMetrizableSpace.regularSpace` `UniformSpace.pseudoMetrizableSpace` `EMetric.instIsCountablyGeneratedUniformity`

---

← Back to Index