Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-02-10 16:32 93ba8b6d

View on Github →

refactor(topology/metric_space): introduce&use edist/dist bases (#1969)

  • refactor(topology/metric_space): introduce&use edist/dist bases
  • Introduce bases for emetric_space and metric_space.
  • Make some proofs use general facts about filter bases.
  • Fix some lint errors
  • Update src/topology/metric_space/emetric_space.lean Co-Authored-By: sgouezel [email protected]
  • +2 docstrings

Estimated changes

deleted theorem metric.mem_closure_iff'
added theorem metric.mem_closure_iff
added theorem metric.nhds_basis_ball
deleted theorem metric.nhds_eq
deleted theorem metric.uniformity_dist'
deleted theorem metric.uniformity_dist
deleted theorem uniformity_edist
deleted theorem emetric.mem_closure_iff'
modified theorem emetric.mem_nhds_iff
modified theorem emetric.nhds_eq
added theorem uniformity_basis_edist
deleted theorem uniformity_edist''
deleted theorem uniformity_edist'
added theorem uniformity_edist
deleted theorem uniformity_edist_inv_nat
deleted theorem uniformity_edist_nnreal
added theorem nhds_basis_uniformity'
added theorem nhds_basis_uniformity
added theorem cauchy_iff'
deleted theorem cauchy_seq_iff_prod_map
added theorem cauchy_seq_iff_tendsto