Commit 2023-11-14 14:30 e6e9cec4

View on Github →

chore(Topology/UniformSpace): change defeq (#8334) Make toTopologicalSpace_top a rfl. Also move some lemmas to the UniformSpace namespace.

Estimated changes

Modified Mathlib/Analysis/LocallyConvex/WithSeminorms.lean

Modified Mathlib/Topology/UniformSpace/Basic.lean

added theorem UniformSpace.toTopologicalSpace_bot

added theorem UniformSpace.toTopologicalSpace_comap

added theorem UniformSpace.toTopologicalSpace_iInf

added theorem UniformSpace.toTopologicalSpace_inf

added theorem UniformSpace.toTopologicalSpace_mono

added theorem UniformSpace.toTopologicalSpace_sInf

added theorem UniformSpace.toTopologicalSpace_top

added theorem UniformSpace.to_nhds_mono

added theorem bot_uniformity

modified theorem inf_uniformity

deleted theorem toTopologicalSpace_bot

deleted theorem toTopologicalSpace_comap

deleted theorem toTopologicalSpace_iInf

deleted theorem toTopologicalSpace_inf

deleted theorem toTopologicalSpace_mono

deleted theorem toTopologicalSpace_sInf

deleted theorem toTopologicalSpace_top

deleted theorem to_nhds_mono

added theorem top_uniformity

Modified Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean