Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-08-26 15:40 5b3b136a

View on Github →

feat(topology): port metric space from lean2

Estimated changes

added theorem abs_eq_zero_iff
added theorem dense
added theorem eq_of_le_of_forall_ge
added theorem eq_of_le_of_forall_le
added theorem le_of_forall_ge
added theorem le_of_forall_le
added theorem no_bot
added theorem no_top
deleted theorem lattice.foo'
deleted theorem lattice.foo
added theorem lattice.inf_infi
added theorem lattice.infi_inf
modified theorem filter.mem_prod_iff
modified theorem filter.mem_prod_same_iff
modified theorem filter.prod_comm
added theorem filter.prod_def
added theorem filter.prod_infi_left
added theorem filter.prod_infi_right
modified theorem filter.prod_mem_prod
modified theorem filter.prod_same_eq
added theorem filter.tendsto_infi'
added theorem filter.tendsto_infi
added def closed_ball
added theorem continuous_dist'
added theorem continuous_dist
added def dist
added theorem dist_comm
added theorem dist_eq_zero_iff
added theorem dist_nonneg
added theorem dist_pos_of_ne
added theorem dist_self
added theorem dist_triangle
added theorem eq_of_dist_eq_zero
added theorem eq_of_forall_dist_le
added theorem exists_subtype
added theorem is_closed_closed_ball
added theorem is_open_metric
added theorem is_open_open_ball
added theorem mem_open_ball
added theorem ne_of_dist_pos
added theorem nhds_eq_metric
added def open_ball
added theorem pos_of_mem_open_ball
added theorem tendsto_dist
added theorem uniformity_dist'
added theorem uniformity_dist
added theorem zero_eq_dist_iff
deleted theorem zero_lt_two