Commit 2023-09-14 17:32 8266eb71

View on Github →

feat: piCongr for topological and uniform spaces (#6836)

Estimated changes

Modified Mathlib/Topology/Constructions.lean

added theorem Pi.continuous_postcomp'

added theorem Pi.continuous_postcomp

added theorem Pi.continuous_precomp'

added theorem Pi.continuous_precomp

added theorem Pi.continuous_restrict

added theorem Pi.induced_precomp'

added theorem Pi.induced_precomp

added theorem Pi.induced_restrict

Modified Mathlib/Topology/Homeomorph.lean

added def Homeomorph.piCongr

added def Homeomorph.piCongrLeft

Modified Mathlib/Topology/UniformSpace/Equiv.lean

added def UniformEquiv.piCongr

added def UniformEquiv.piCongrLeft

added def UniformEquiv.piCongrRight

added theorem UniformEquiv.piCongrRight_symm

Modified Mathlib/Topology/UniformSpace/Pi.lean

added theorem Pi.uniformContinuous_postcomp'

added theorem Pi.uniformContinuous_postcomp

added theorem Pi.uniformContinuous_precomp'

added theorem Pi.uniformContinuous_precomp

added theorem Pi.uniformContinuous_restrict

added theorem Pi.uniformSpace_comap_precomp'

added theorem Pi.uniformSpace_comap_precomp

added theorem Pi.uniformSpace_comap_restrict