Basic

📁 Source: Mathlib/Topology/EMetricSpace/Basic.lean

Statistics

Metric	Count
Definitions ofT0PseudoEMetricSpace, emetricSpaceMax, instEDistSeparationQuotient, instEMetricSpaceSeparationQuotient	4
Theorems cauchySeq_iff, cauchySeq_iff', cauchySeq_iff_NNReal, cauchy_iff, complete_of_cauchySeq_tendsto, complete_of_convergent_controlled_sequences, controlled_of_isUniformEmbedding, countable_closure_of_compact, inseparable_iff, instNontrivialTopologyOfNontrivial, isUniformEmbedding_iff, isUniformEmbedding_iff', isUniformInducing_iff, nontrivial_iff_nontrivialTopology, secondCountable_of_almost_dense_set, secondCountable_of_sigmaCompact, subset_countable_closure_of_almost_dense_set, subset_countable_closure_of_compact, subsingleton_iff_indiscreteTopology, tendstoLocallyUniformlyOn_iff, tendstoLocallyUniformly_iff, tendstoUniformlyOn_iff, tendstoUniformly_iff, totallyBounded_iff, totallyBounded_iff', instT0Space, edist_eq_zero, edist_mk, edist_le_Ico_sum_edist, edist_le_Ico_sum_of_edist_le, edist_le_range_sum_edist, edist_le_range_sum_of_edist_le, lebesgue_number_lemma_of_emetric, lebesgue_number_lemma_of_emetric_nhds, lebesgue_number_lemma_of_emetric_nhds', lebesgue_number_lemma_of_emetric_nhdsWithin, lebesgue_number_lemma_of_emetric_nhdsWithin', lebesgue_number_lemma_of_emetric_sUnion	38
Total	42

EMetric

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cauchySeq_iff 📖	mathematical	—	CauchySeq PseudoEMetricSpace.toUniformSpace PartialOrder.toPreorder SemilatticeSup.toPartialOrder ENNReal Preorder.toLT ENNReal.instPartialOrder EDist.edist PseudoEMetricSpace.toEDist	—	Filter.HasBasis.cauchySeq_iff uniformity_basis_edist
cauchySeq_iff' 📖	mathematical	—	CauchySeq PseudoEMetricSpace.toUniformSpace PartialOrder.toPreorder SemilatticeSup.toPartialOrder ENNReal Preorder.toLT ENNReal.instPartialOrder EDist.edist PseudoEMetricSpace.toEDist	—	Filter.HasBasis.cauchySeq_iff' uniformity_basis_edist
cauchySeq_iff_NNReal 📖	mathematical	—	CauchySeq PseudoEMetricSpace.toUniformSpace PartialOrder.toPreorder SemilatticeSup.toPartialOrder ENNReal Preorder.toLT ENNReal.instPartialOrder EDist.edist PseudoEMetricSpace.toEDist ENNReal.ofNNReal	—	Filter.HasBasis.cauchySeq_iff' uniformity_basis_edist_nnreal
cauchy_iff 📖	mathematical	—	Cauchy PseudoEMetricSpace.toUniformSpace Set Filter Filter.instMembership ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist PseudoEMetricSpace.toEDist	—	Filter.neBot_iff Filter.HasBasis.cauchy_iff uniformity_basis_edist
complete_of_cauchySeq_tendsto 📖	mathematical	Filter.Tendsto Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace	CompleteSpace	—	UniformSpace.complete_of_cauchySeq_tendsto instIsCountablyGeneratedUniformity
complete_of_convergent_controlled_sequences 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal Filter.Tendsto Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace	CompleteSpace	—	UniformSpace.complete_of_convergent_controlled_sequences instIsCountablyGeneratedUniformity edist_mem_uniformity
controlled_of_isUniformEmbedding 📖	mathematical	IsUniformEmbedding PseudoEMetricSpace.toUniformSpace	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal EDist.edist PseudoEMetricSpace.toEDist	—	uniformContinuous_iff IsUniformInducing.uniformContinuous IsUniformEmbedding.toIsUniformInducing isUniformEmbedding_iff
countable_closure_of_compact 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace EMetricSpace.toPseudoEMetricSpace	Set Set.instHasSubset Set.Countable closure	—	subset_countable_closure_of_compact HasSubset.Subset.antisymm Set.instAntisymmSubset closure_minimal IsCompact.isClosed T25Space.t2Space T3Space.t25Space T4Space.t3Space instT4SpaceOfT1SpaceOfNormalSpace instT1SpaceOfT0SpaceOfR0Space EMetricSpace.instT0Space instR0Space instR1Space UniformSpace.to_regularSpace CompletelyNormalSpace.toNormalSpace UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity instIsCountablyGeneratedUniformity
inseparable_iff 📖	mathematical	—	Inseparable UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace EDist.edist PseudoEMetricSpace.toEDist ENNReal instZeroENNReal	—	ENNReal.instCanonicallyOrderedAdd PseudoEMetricSpace.edist_comm
instNontrivialTopologyOfNontrivial 📖	mathematical	—	NontrivialTopology UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace EMetricSpace.toPseudoEMetricSpace	—	nontrivial_iff_nontrivialTopology
isUniformEmbedding_iff 📖	mathematical	—	IsUniformEmbedding PseudoEMetricSpace.toUniformSpace UniformContinuous ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal EDist.edist PseudoEMetricSpace.toEDist	—	isUniformEmbedding_iff Iff.and isUniformInducing_iff
isUniformEmbedding_iff' 📖	mathematical	—	IsUniformEmbedding PseudoEMetricSpace.toUniformSpace EMetricSpace.toPseudoEMetricSpace ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal EDist.edist PseudoEMetricSpace.toEDist	—	isUniformEmbedding_iff_isUniformInducing EMetricSpace.instT0Space isUniformInducing_iff uniformContinuous_iff
isUniformInducing_iff 📖	mathematical	—	IsUniformInducing PseudoEMetricSpace.toUniformSpace UniformContinuous ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal EDist.edist PseudoEMetricSpace.toEDist	—	isUniformInducing_iff' Iff.and Filter.HasBasis.le_basis_iff Filter.HasBasis.comap uniformity_basis_edist
nontrivial_iff_nontrivialTopology 📖	mathematical	—	Nontrivial NontrivialTopology UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace EMetricSpace.toPseudoEMetricSpace	—	—
secondCountable_of_almost_dense_set 📖	mathematical	Set.Countable Set.iUnion Set Set.instMembership Metric.closedEBall Set.univ	SecondCountableTopology UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace	—	subset_countable_closure_of_almost_dense_set Set.mem_univ UniformSpace.secondCountable_of_separable instIsCountablyGeneratedUniformity
secondCountable_of_sigmaCompact 📖	mathematical	—	SecondCountableTopology UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace	—	Set.countable_iUnion instCountableNat Set.iUnion_eq_univ_iff iUnion_compactCovering closure_mono Set.subset_iUnion subset_countable_closure_of_compact isCompact_compactCovering UniformSpace.secondCountable_of_separable instIsCountablyGeneratedUniformity
subset_countable_closure_of_almost_dense_set 📖	mathematical	Set.Countable Set Set.instHasSubset Set.iUnion Set.instMembership Metric.closedEBall	closure UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace	—	UniformSpace.subset_countable_closure_of_almost_dense_set instIsCountablyGeneratedUniformity Filter.HasBasis.mem_iff uniformity_basis_edist_le HasSubset.Subset.trans Set.instIsTransSubset Set.iUnion₂_mono UniformSpace.ball_mono PseudoEMetricSpace.edist_comm Metric.mem_closedEBall
subset_countable_closure_of_compact 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace	Set Set.instHasSubset Set.Countable closure	—	subset_countable_closure_of_almost_dense_set totallyBounded_iff' IsCompact.totallyBounded Set.Finite.countable HasSubset.Subset.trans Set.instIsTransSubset Set.iUnion₂_mono Metric.eball_subset_closedEBall
subsingleton_iff_indiscreteTopology 📖	mathematical	—	IndiscreteTopology UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace EMetricSpace.toPseudoEMetricSpace	—	Iff.not nontrivial_iff_nontrivialTopology
tendstoLocallyUniformlyOn_iff 📖	mathematical	—	TendstoLocallyUniformlyOn PseudoEMetricSpace.toUniformSpace Set Filter Filter.instMembership nhdsWithin Filter.Eventually	—	edist_mem_uniformity mem_uniformity_edist Filter.Eventually.mono
tendstoLocallyUniformly_iff 📖	mathematical	—	TendstoLocallyUniformly PseudoEMetricSpace.toUniformSpace Set Filter Filter.instMembership nhds Filter.Eventually	—	nhdsWithin_univ
tendstoUniformlyOn_iff 📖	mathematical	—	TendstoUniformlyOn PseudoEMetricSpace.toUniformSpace Filter.Eventually	—	edist_mem_uniformity mem_uniformity_edist Filter.Eventually.mono
tendstoUniformly_iff 📖	mathematical	—	TendstoUniformly PseudoEMetricSpace.toUniformSpace Filter.Eventually	—	—
totallyBounded_iff 📖	mathematical	—	TotallyBounded PseudoEMetricSpace.toUniformSpace Set.Finite Set Set.instHasSubset Set.iUnion Set.instMembership Metric.eball	—	edist_mem_uniformity mem_uniformity_edist HasSubset.Subset.trans Set.instIsTransSubset Set.iUnion₂_mono
totallyBounded_iff' 📖	mathematical	—	TotallyBounded PseudoEMetricSpace.toUniformSpace Set Set.instHasSubset Set.Finite Set.iUnion Set.instMembership Metric.eball	—	totallyBounded_iff_subset edist_mem_uniformity mem_uniformity_edist HasSubset.Subset.trans Set.instIsTransSubset Set.iUnion₂_mono

EMetricSpace

Definitions

Name	Category	Theorems
ofT0PseudoEMetricSpace 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instT0Space 📖	mathematical	—	T0Space UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace toPseudoEMetricSpace	—	eq_of_edist_eq_zero EMetric.inseparable_iff

Inseparable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
edist_eq_zero 📖	mathematical	Inseparable UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace	EDist.edist PseudoEMetricSpace.toEDist ENNReal instZeroENNReal	—	EMetric.inseparable_iff

Prod

Definitions

Name	Category	Theorems
emetricSpaceMax 📖	CompOp	5 math math: EMetric.NonemptyCompacts.lipschitz_prod, TopologicalSpace.Compacts.lipschitz_prod, MeasureTheory.hausdorffMeasure_measurePreserving_piFinTwo, TopologicalSpace.NonemptyCompacts.lipschitz_prod, MeasureTheory.hausdorffMeasure_prod_real

SeparationQuotient

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
edist_mk 📖	mathematical	—	EDist.edist SeparationQuotient UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace instEDistSeparationQuotient PseudoEMetricSpace.toEDist	—	—

(root)

Definitions

Name	Category	Theorems
instEDistSeparationQuotient 📖	CompOp	1 math math: SeparationQuotient.edist_mk
instEMetricSpaceSeparationQuotient 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
edist_le_Ico_sum_edist 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist PseudoEMetricSpace.toEDist Finset.sum ENNReal.instAddCommMonoid Finset.Ico Nat.instPreorder Nat.instLocallyFiniteOrder	—	Nat.le_induction Finset.Ico_self Finset.sum_empty PseudoEMetricSpace.edist_self le_refl PseudoEMetricSpace.edist_triangle add_le_add IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add le_rfl Finset.insert_Ico_right_eq_Ico_add_one Nat.instNoMaxOrder Finset.sum_insert add_comm
edist_le_Ico_sum_of_edist_le 📖	mathematical	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist PseudoEMetricSpace.toEDist	Finset.sum ENNReal.instAddCommMonoid Finset.Ico Nat.instPreorder Nat.instLocallyFiniteOrder	—	le_trans edist_le_Ico_sum_edist Finset.sum_le_sum IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid Finset.mem_Ico
edist_le_range_sum_edist 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist PseudoEMetricSpace.toEDist Finset.sum ENNReal.instAddCommMonoid Finset.range	—	edist_le_Ico_sum_edist Nat.Ico_zero_eq_range
edist_le_range_sum_of_edist_le 📖	mathematical	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist PseudoEMetricSpace.toEDist	Finset.sum ENNReal.instAddCommMonoid Finset.range	—	edist_le_Ico_sum_of_edist_le zero_le Nat.instCanonicallyOrderedAdd Nat.Ico_zero_eq_range
lebesgue_number_lemma_of_emetric 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace IsOpen Set Set.instHasSubset Set.iUnion	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal Metric.eball	—	PseudoEMetricSpace.edist_comm Filter.HasBasis.lebesgue_number_lemma uniformity_basis_edist
lebesgue_number_lemma_of_emetric_nhds 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace Set Filter Filter.instMembership nhds	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal Set.instHasSubset Metric.eball	—	PseudoEMetricSpace.edist_comm Filter.HasBasis.lebesgue_number_lemma_nhds uniformity_basis_edist
lebesgue_number_lemma_of_emetric_nhds' 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace Set Filter Filter.instMembership nhds	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal Set.instHasSubset Metric.eball Set.instMembership	—	PseudoEMetricSpace.edist_comm Filter.HasBasis.lebesgue_number_lemma_nhds' uniformity_basis_edist
lebesgue_number_lemma_of_emetric_nhdsWithin 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace Set Filter Filter.instMembership nhdsWithin	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal Set.instHasSubset Set.instInter Metric.eball	—	PseudoEMetricSpace.edist_comm Filter.HasBasis.lebesgue_number_lemma_nhdsWithin uniformity_basis_edist
lebesgue_number_lemma_of_emetric_nhdsWithin' 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace Set Filter Filter.instMembership nhdsWithin	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal Set.instHasSubset Set.instInter Metric.eball Set.instMembership	—	PseudoEMetricSpace.edist_comm Filter.HasBasis.lebesgue_number_lemma_nhdsWithin' uniformity_basis_edist
lebesgue_number_lemma_of_emetric_sUnion 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace IsOpen Set Set.instHasSubset Set.sUnion	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal Set.instMembership Metric.eball	—	lebesgue_number_lemma_of_emetric Set.sUnion_eq_iUnion

---

← Back to Index