Commit 2023-08-22 13:23 db373a75

View on Github →

chore: more predictable ext lemmas for TopologicalSpace and UniformSpace (#6705)

Estimated changes

Modified Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

Modified Mathlib/Topology/Algebra/Group/Basic.lean

Modified Mathlib/Topology/Algebra/Ring/Basic.lean

Modified Mathlib/Topology/Algebra/UniformGroup.lean

Modified Mathlib/Topology/Algebra/Valuation.lean

Modified Mathlib/Topology/Basic.lean

deleted theorem topologicalSpace_eq

deleted theorem topologicalSpace_eq_iff

Modified Mathlib/Topology/Maps.lean

Modified Mathlib/Topology/MetricSpace/Basic.lean

Modified Mathlib/Topology/MetricSpace/EMetricSpace.lean

Modified Mathlib/Topology/MetricSpace/MetrizableUniformity.lean

Modified Mathlib/Topology/Order.lean

Modified Mathlib/Topology/Order/UpperLowerSetTopology.lean

Modified Mathlib/Topology/UniformSpace/Basic.lean

added theorem UniformSpace.Core.ext

deleted theorem UniformSpace.core_eq

deleted theorem uniformSpace_eq

Modified Mathlib/Topology/UniformSpace/Compact.lean

Modified Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean

Modified Mathlib/Topology/UniformSpace/UniformEmbedding.lean