Commit 2026-01-28 00:28 a33bfcd2

View on Github →

feat(StrongTopology): add IsInducing lemmas (#34497) Also get rid of some _s in definition names and move the definitions of IsUniformInducing/IsUniformEmbedding to Defs.lean. I'm going to use these results to transfer more theorems about ContinuousMultilinearMaps, including the ones from #34491, to ContinuousAlternatingMaps.

Estimated changes

added structure IsUniformEmbedding
added structure IsUniformInducing
modified theorem UniformContinuous.iterate
modified def UniformContinuous
modified def UniformContinuousOn
modified theorem uniformContinuousOn_univ
modified theorem uniformContinuous_const
modified theorem uniformContinuous_def
modified theorem uniformContinuous_of_const
deleted structure IsUniformEmbedding
deleted structure IsUniformInducing