Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-02-08 09:28 b2ba37c7

View on Github →

chore(*): fix errors introduced by rebasing

Estimated changes

deleted theorem abs_dist
deleted theorem abs_dist_sub_le
deleted def ball
deleted theorem ball_disjoint
deleted theorem ball_disjoint_same
deleted theorem ball_eq_empty_iff_nonpos
deleted theorem ball_half_subset
deleted theorem ball_mem_nhds
deleted theorem ball_subset
deleted theorem ball_subset_ball
deleted theorem ball_subset_closed_ball
deleted theorem cauchy_of_metric
deleted theorem cauchy_seq_metric'
deleted theorem cauchy_seq_metric
deleted def closed_ball
deleted theorem continuous_dist'
deleted theorem continuous_dist
deleted theorem continuous_of_metric
deleted theorem continuous_topo_metric
deleted theorem dist_comm
deleted theorem dist_eq_edist
deleted theorem dist_eq_nndist
deleted theorem dist_eq_zero
deleted theorem dist_le_zero
deleted theorem dist_mem_uniformity
deleted theorem dist_nonneg
deleted theorem dist_pi_def
deleted theorem dist_pos
deleted theorem dist_self
deleted theorem dist_triangle
deleted theorem dist_triangle_left
deleted theorem dist_triangle_right
deleted theorem edist_dist
deleted theorem edist_eq_dist
deleted theorem edist_eq_nndist
deleted theorem edist_ne_top
deleted theorem eq_of_dist_eq_zero
deleted theorem eq_of_forall_dist_le
deleted theorem eq_of_nndist_eq_zero
deleted theorem exists_ball_subset_ball
deleted theorem is_closed_ball
deleted theorem is_open_ball
deleted theorem is_open_metric
deleted theorem mem_ball'
deleted theorem mem_ball
deleted theorem mem_ball_comm
deleted theorem mem_ball_self
deleted theorem mem_closed_ball
deleted theorem mem_closure_iff'
deleted theorem mem_nhds_iff_metric
deleted theorem mem_uniformity_dist
deleted theorem mem_uniformity_dist_edist
deleted theorem metric.mem_nhds_within
deleted theorem nhds_comap_dist
deleted theorem nhds_eq_metric
deleted def nndist
deleted theorem nndist_comm
deleted theorem nndist_eq_dist
deleted theorem nndist_eq_edist
deleted theorem nndist_eq_zero
deleted theorem nndist_self
deleted theorem nndist_triangle
deleted theorem nndist_triangle_left
deleted theorem nndist_triangle_right
deleted theorem pos_of_mem_ball
deleted theorem real.dist_0_eq_abs
deleted theorem real.dist_eq
deleted theorem subtype.dist_eq
deleted theorem swap_dist
deleted theorem tendsto_at_top_metric
deleted theorem tendsto_dist
deleted theorem tendsto_nhds_of_metric
deleted theorem tendsto_nhds_topo_metric
deleted theorem totally_bounded_of_metric
deleted theorem uniform_continuous_dist'
deleted theorem uniform_continuous_dist
deleted theorem uniformity_dist'
deleted theorem uniformity_dist
deleted theorem uniformity_edist'
deleted theorem uniformity_edist
deleted theorem zero_eq_dist
deleted theorem zero_eq_nndist
deleted theorem cau_seq_iff_cauchy_seq
deleted theorem cauchy_of_filter_cauchy
deleted theorem filter_cauchy_of_cauchy
deleted theorem tendsto_limit
modified def continuous_at_within
modified theorem continuous_at_within_univ