Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-20 20:42 2c5bc214

View on Github →

feat(topology/emetric_space): basic facts for emetric spaces (#608)

Estimated changes

Modified src/topology/metric_space/basic.lean

deleted theorem countable_closure_of_compact

deleted theorem second_countable_of_separable_metric_space

Modified src/topology/metric_space/emetric_space.lean

added theorem edist_triangle4

added def emetric.ball

added theorem emetric.ball_disjoint

added theorem emetric.ball_mem_nhds

added theorem emetric.ball_subset

added theorem emetric.ball_subset_ball

added theorem emetric.ball_subset_closed_ball

deleted theorem emetric.cauchy_iff

added theorem emetric.cauchy_seq_iff'

added theorem emetric.cauchy_seq_iff

added def emetric.closed_ball

added theorem emetric.closed_ball_subset_closed_ball

added theorem emetric.countable_closure_of_compact

added theorem emetric.exists_ball_subset_ball

added theorem emetric.is_open_ball

added theorem emetric.is_open_iff

added theorem emetric.mem_ball'

added theorem emetric.mem_ball

added theorem emetric.mem_ball_comm

added theorem emetric.mem_ball_self

added theorem emetric.mem_closed_ball

added theorem emetric.mem_closure_iff'

added theorem emetric.mem_nhds_iff

added theorem emetric.nhds_eq

added theorem emetric.pos_of_mem_ball

added theorem emetric.second_countable_of_separable

added theorem emetric.tendsto_at_top

added theorem emetric.tendsto_nhds

added theorem emetric.totally_bounded_iff'

added theorem emetric.totally_bounded_iff