Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-14 13:34 49c059a4

View on Github →

refactor(analysis): add metric namespace combines changes from @sgouezel, @PatrickMassot, and @digama0

Estimated changes

added theorem edist_eq_zero
added theorem edist_mem_uniformity
added theorem edist_triangle_left
added theorem edist_triangle_right
added theorem emetric.cauchy_iff
modified def emetric_space.induced
added theorem eq_of_forall_edist_le
added theorem mem_uniformity_edist
added theorem subtype.edist_eq
added theorem uniformity_edist''
added theorem uniformity_edist'
added theorem zero_eq_edist
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 bounded.subset
deleted def bounded
deleted theorem bounded_bUnion
deleted theorem bounded_ball
deleted theorem bounded_closed_ball
deleted theorem bounded_empty
deleted theorem bounded_iff_mem_bounded
deleted theorem bounded_iff_subset_ball
deleted theorem bounded_of_compact
deleted theorem bounded_of_compact_space
deleted theorem bounded_of_finite
deleted theorem bounded_range_iff
deleted theorem bounded_singleton
deleted theorem bounded_union
deleted theorem cauchy_of_metric
deleted theorem cauchy_seq_metric'
deleted theorem cauchy_seq_metric
deleted def closed_ball
deleted theorem continuous_of_metric
deleted theorem continuous_topo_metric
deleted theorem dist_mem_uniformity
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_of_closed'
deleted theorem mem_uniformity_dist
deleted theorem mem_uniformity_dist_edist
added def metric.ball
added theorem metric.ball_disjoint
added theorem metric.ball_mem_nhds
added theorem metric.ball_subset
added theorem metric.bounded.subset
added def metric.bounded
added theorem metric.bounded_bUnion
added theorem metric.bounded_ball
added theorem metric.bounded_empty
added theorem metric.bounded_union
added theorem metric.cauchy_seq_iff'
added theorem metric.cauchy_seq_iff
added theorem metric.continuous_iff'
added theorem metric.continuous_iff
added theorem metric.is_closed_ball
added theorem metric.is_open_ball
added theorem metric.is_open_iff
added theorem metric.mem_ball'
added theorem metric.mem_ball
added theorem metric.mem_ball_comm
added theorem metric.mem_ball_self
added theorem metric.mem_closed_ball
added theorem metric.mem_nhds_iff
added theorem metric.mem_of_closed'
added theorem metric.nhds_eq
added theorem metric.pos_of_mem_ball
added theorem metric.tendsto_at_top
added theorem metric.tendsto_nhds
added theorem metric.uniformity_dist
deleted theorem nhds_eq_metric
deleted theorem pos_of_mem_ball
deleted theorem tendsto_at_top_metric
deleted theorem tendsto_nhds_of_metric
deleted theorem tendsto_nhds_topo_metric
deleted theorem totally_bounded_of_metric
deleted theorem uniformity_dist'
deleted theorem uniformity_dist
deleted theorem uniformity_edist'