Mathlib v3 is deprecated. Go to Mathlib v4

Theorem metric.pos_of_mem_ball

Modification history

2020-06-04 04:42

src/topology/metric_space/basic.lean

chore(*): fix some `ge_or_gt` lint issues (#2945) …

Modified metric.pos_of_mem_ball View on Github →

2019-01-14 13:34

analysis/metric_space.lean

refactor(analysis): add metric namespace …

Added metric.pos_of_mem_ball View on Github →