Commit 2026-04-02 11:54 507f3af6

View on Github →

feat(Topology/EMetricSpace/Basic): generalize lemma (#37529) Generalize the lemma controlled_of_isUniformEmbedding to uniform inducing maps. This resolves a TODO.

Estimated changes

Modified Mathlib/Topology/EMetricSpace/Basic.lean

added theorem EMetric.controlled_of_isUniformInducing

Modified Mathlib/Topology/MetricSpace/Pseudo/Basic.lean

added theorem Metric.controlled_of_isUniformInducing