Commit 2026-08-13 16:41 f7ae959e

View on Github →

feat(Topology): generalize basic files to Weak(Pseudo)EMetricSpace (#42688) Similar to #42662

Estimated changes

Modified Mathlib/Topology/EMetricSpace/Basic.lean

modified theorem EMetric.cauchySeq_iff'

modified theorem EMetric.cauchySeq_iff

modified theorem EMetric.cauchySeq_iff_NNReal

modified theorem EMetric.controlled_of_isUniformEmbedding

modified theorem EMetric.controlled_of_isUniformInducing

modified theorem EMetric.inseparable_iff

modified theorem EMetric.isUniformInducing_iff

modified theorem EMetric.subset_countable_closure_of_compact

modified theorem EMetric.tendstoLocallyUniformlyOn_iff

modified theorem EMetric.tendstoLocallyUniformly_iff

modified theorem EMetric.tendstoUniformlyOn_iff

modified theorem EMetric.tendstoUniformly_iff

modified theorem EMetric.totallyBounded_iff'

modified theorem EMetric.totallyBounded_iff

modified theorem lebesgue_number_lemma_of_emetric

modified theorem lebesgue_number_lemma_of_emetric_nhds'

modified theorem lebesgue_number_lemma_of_emetric_nhds

modified theorem lebesgue_number_lemma_of_emetric_nhdsWithin'

modified theorem lebesgue_number_lemma_of_emetric_nhdsWithin

modified theorem lebesgue_number_lemma_of_emetric_sUnion

Modified Mathlib/Topology/EMetricSpace/Diam.lean

Modified Mathlib/Topology/EMetricSpace/MulOpposite.lean

Modified Mathlib/Topology/EMetricSpace/PairReduction.lean

modified theorem EMetric.pair_reduction

modified theorem PairReduction.iSup_edist_pairSet

Modified Mathlib/Topology/EMetricSpace/Pi.lean

Modified Mathlib/Topology/MetricSpace/MetricSeparated.lean