Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-11 18:01 5f098cfd

View on Github →

chore(topology): 2 trivial lemmas (#4968)

Estimated changes

Modified src/analysis/normed_space/basic.lean

added theorem mem_ball_iff_norm'

added theorem mem_ball_iff_norm

added theorem mem_closed_ball_iff_norm'

added theorem mem_closed_ball_iff_norm

Modified src/topology/bases.lean

added theorem topological_space.is_topological_basis.nhds_has_basis

Modified src/topology/metric_space/basic.lean

added theorem metric.eventually_nhds_iff

added theorem metric.eventually_nhds_iff_ball

added theorem metric.mem_closed_ball'