Mathlib Changelog
v3
Changelog
About
Github
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
Modified
algebra/field.lean
Modified
algebra/group.lean
added
theorem
abs_eq_zero_iff
Modified
data/rat.lean
Modified
order/basic.lean
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
Modified
order/complete_lattice.lean
deleted
theorem
lattice.foo'
deleted
theorem
lattice.foo
added
theorem
lattice.inf_infi
added
theorem
lattice.infi_inf
Modified
order/filter.lean
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
theorem
filter.tendsto_principal_principal
Created
topology/metric_space.lean
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_nhds_sets_iff_metric
added
theorem
mem_open_ball
added
theorem
ne_of_dist_pos
added
theorem
nhds_eq_metric
added
def
open_ball
added
theorem
open_ball_eq_empty_of_nonpos
added
theorem
open_ball_subset_open_ball_of_le
added
theorem
pos_of_mem_open_ball
added
theorem
tendsto_dist
added
theorem
uniform_continuous_dist'
added
theorem
uniform_continuous_dist
added
theorem
uniformity_dist'
added
theorem
uniformity_dist
added
theorem
zero_eq_dist_iff
Modified
topology/real.lean
deleted
theorem
zero_lt_two
Modified
topology/uniform_space.lean
added
theorem
uniformity_prod_eq_prod