Commit 2023-02-04 09:44 8b2fe789

View on Github →

feat: Port Topology.UniformSpace.AbsoluteValue (#2044)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/UniformSpace/AbsoluteValue.lean

added theorem IsAbsoluteValue.mem_uniformity

added def IsAbsoluteValue.uniformSpace

added def IsAbsoluteValue.uniformSpaceCore