Commit 2025-09-19 12:18 d8a594d0

View on Github →

feat(Topology/UniformSpace/Path): new file (#24105)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Topology/ContinuousMap/Defs.lean

Modified Mathlib/Topology/Path.lean

added theorem Path.range_coe

Modified Mathlib/Topology/UniformSpace/CompactConvergence.lean

added theorem ContinuousMap.isComplete_setOf_eqOn

Created Mathlib/Topology/UniformSpace/Path.lean

added theorem Filter.HasBasis.uniformityPath

added theorem Path.hasBasis_uniformity

added theorem Path.isUniformEmbedding_coe

added theorem Path.uniformContinuous

added theorem Path.uniformContinuous_extend

added theorem Path.uniformContinuous_extend_left

added theorem Path.uniformContinuous_symm

added theorem Path.uniformContinuous_trans