Commit 2025-04-28 07:37 c7cf6b6e

refactor(Topology/UniformSpace): clarify def of TendstoLocallyUniformly (#24342) Split Mathlib.Topology.UniformSpace.UniformConvergence into 3 files, and add a detailed explanation of how our definition of TendstoLocallyUniformly differs from the one usually found in the literature. See discussion on Zulip: https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/Locally.20uniform.20convergence/with/514097469