Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-02-22 16:24 1c6a317a

View on Github →

feat(*): misc simple lemmas (#2036)

feat(*): misc simple lemmas
+1 lemma
Rename inclusion_range to range_inclusion Co-Authored-By: Johan Commelin johan@commelin.net

Estimated changes

Modified src/analysis/normed_space/basic.lean

added theorem nndist_smul

Modified src/data/set/basic.lean

added theorem set.range_inclusion

Modified src/order/filter/basic.lean

added theorem filter.comap_ne_bot_of_image_mem

Modified src/topology/metric_space/emetric_space.lean

added theorem emetric.is_closed_ball_top

added theorem prod.edist_eq