Commit 2026-10-14 00:41 f9254e25

View on Github →

feat: pushforward of uniform spaces (#43312) We define the pushforward of uniforms spaces and show it is left adjoint to the pullback.

Estimated changes

Modified Mathlib/Topology/Algebra/Module/Spaces/UniformConvergenceCLM.lean

Modified Mathlib/Topology/UniformSpace/Ascoli.lean

Modified Mathlib/Topology/UniformSpace/Basic.lean

added theorem UniformSpace.comap_id

deleted theorem UniformSpace.comap_mono

added theorem UniformSpace.comap_monotone

added theorem UniformSpace.gc_generateFilter_uniformity

added theorem UniformSpace.gc_map_comap

added def UniformSpace.generateFilter

added def UniformSpace.giGenerateFilter

added def UniformSpace.map

added theorem UniformSpace.map_iSup

added theorem UniformSpace.map_id

added theorem UniformSpace.map_map

added theorem UniformSpace.map_monotone

added theorem UniformSpace.map_sup

added theorem UniformSpace.mem_uniformity_generateFilter

added theorem uniformContinuous_iff_map_le

added theorem uniformContinuous_map'

added theorem uniformContinuous_map

deleted theorem uniformSpace_comap_id

Modified Mathlib/Topology/UniformSpace/Cauchy.lean

Modified Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean