Commit 2025-02-16 16:41 d271b494

View on Github →

feat: instance NormedField.instCompletableTopField (#20686) This adds the missing instance NormedField → CompletableTopField. See here on Zulip. This needs to import both Mathlib.Topology.Algebra.UniformField and Mathlib.Analysis.Normed.Field.Lemmas, which so far no file does, so I've opted to create a new file Mathlib.Analysis.Normed.Field.Instances to house it. Following suggestions made while discussing this PR, it also adds some API lemmas for filters.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Normed/Field/Instances.lean

Modified Mathlib/Analysis/Normed/Group/Basic.lean

added theorem SeminormedGroup.disjoint_nhds

added theorem SeminormedGroup.disjoint_nhds_one

Modified Mathlib/Order/LiminfLimsup.lean

added theorem Filter.Tendsto.isBoundedUnder_comp

added theorem Filter.isBoundedUnder_map_iff

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

added theorem UniformGroup.cauchy_iff_tendsto

added theorem UniformGroup.cauchy_iff_tendsto_swapped

added theorem UniformGroup.cauchy_map_iff_tendsto

added theorem UniformGroup.cauchy_map_iff_tendsto_swapped