Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-15 13:26 f5c55aea

View on Github →

feat(analysis/normed_space/basic): uniform_continuous_norm (#6162) From lean-liquid

Estimated changes

Modified src/analysis/asymptotics/asymptotics.lean

Modified src/analysis/normed_space/basic.lean

added theorem dist_zero_left

added theorem lipschitz_with_one_norm

modified theorem real.norm_eq_abs

added theorem uniform_continuous_nnnorm

added theorem uniform_continuous_norm