Mathlib v3 is deprecated. Go to Mathlib v4

Theorem mem_emetric_ball_0_iff

Modification history

2021-09-21 17:41
src/analysis/normed_space/basic.lean
feat(analysis/normed_space/basic): the rescaling of a ball is a ball (#9297) …
Deleted mem_emetric_ball_0_iffView on Github →
2021-06-23 17:29
src/analysis/normed_space/basic.lean
feat(analysis/normed_space/basic): add has_nnnorm (#7986) …
Modified mem_emetric_ball_0_iffView on Github →
2021-02-04 21:33
src/analysis/normed_space/basic.lean
feat(data/real/ennreal): use notation for ennreal (#6044) …
Modified mem_emetric_ball_0_iffView on Github →
2020-12-30 17:33
src/analysis/normed_space/basic.lean
chore(analysis/normed_space/basic): a few lemmas about `nnnorm` (#5532)
Added mem_emetric_ball_0_iffView on Github →