Commit 2024-09-17 23:58 fb04c4bf

View on Github →

feat(Normed/Field): completeSpace_iff_isComplete_closedBall (#15777) On the way to locally complete K iff complete O(K) Also add some helper lemmas about uniform continuity of multiplication by a constant with a variant for rings (via smul) instead of UniformGroup (which fields are not).

Estimated changes

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

added theorem NormedDivisionRing.discreteTopology_unit_closedBall_eq_univ

added theorem NormedDivisionRing.norm_eq_one_iff_ne_zero_of_discrete

added theorem NormedDivisionRing.norm_le_one_of_discrete

Modified Mathlib/Analysis/Normed/Field/Lemmas.lean

added theorem NormedField.completeSpace_iff_isComplete_closedBall

added theorem NormedField.discreteTopology_of_bddAbove_range_norm

added theorem NormedField.discreteTopology_or_nontriviallyNormedField

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

added theorem CauchySeq.mul_norm_bddAbove

Modified Mathlib/Topology/Algebra/UniformGroup.lean

added theorem UniformContinuous.const_mul

added theorem UniformContinuous.div_const

added theorem UniformContinuous.mul_const

added theorem uniformContinuous_div_const

added theorem uniformContinuous_mul_left

added theorem uniformContinuous_mul_right

Modified Mathlib/Topology/Algebra/UniformMulAction.lean

added theorem UniformContinuous.const_mul'

added theorem UniformContinuous.div_const'

added theorem UniformContinuous.mul_const'

added theorem uniformContinuous_div_const'

added theorem uniformContinuous_mul_left'

added theorem uniformContinuous_mul_right'