Commit 2024-09-29 03:18 4cd4cfb8

View on Github →

chore(UniformSpace): move ofFun to a new file (#16737) Also drop @[mono] on hasSum_mono.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Topology/Algebra/InfiniteSum/Order.lean

Modified Mathlib/Topology/ContinuousFunction/Bounded.lean

Modified Mathlib/Topology/EMetricSpace/Defs.lean

Modified Mathlib/Topology/Support.lean

Modified Mathlib/Topology/UniformSpace/AbsoluteValue.lean

Modified Mathlib/Topology/UniformSpace/Basic.lean

deleted theorem UniformSpace.hasBasis_ofFun

deleted def UniformSpace.ofFun

Created Mathlib/Topology/UniformSpace/OfFun.lean

added theorem UniformSpace.hasBasis_ofFun

added def UniformSpace.ofFun

Modified scripts/noshake.json