Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2018-01-19 16:18
bb1a9f2c
View on Github →
feat(data/real,*): supporting material for metric spaces
Estimated changes
Modified
algebra/functions.lean
added
theorem
abs_abs_sub_le_abs_sub
added
theorem
abs_sub_le_iff
added
theorem
abs_sub_lt_iff
added
def
sub_abs_le_abs_sub
Modified
algebra/group.lean
added
theorem
sub_right_comm
added
def
sub_sub_cancel
deleted
theorem
sub_sub_swap
Modified
algebra/module.lean
Modified
algebra/ordered_field.lean
added
theorem
div_le_iff'
added
theorem
div_lt_iff'
added
theorem
le_div_iff'
added
theorem
lt_div_iff'
Modified
algebra/ordered_group.lean
added
theorem
add_neg_le_iff_le_add'
added
theorem
add_neg_le_iff_le_add
added
theorem
le_sub_iff_add_le'
added
theorem
le_sub_iff_add_le
deleted
theorem
le_sub_left_iff_add_le
deleted
theorem
le_sub_right_iff_add_le
added
theorem
lt_sub_iff_add_lt'
added
theorem
lt_sub_iff_add_lt
deleted
theorem
lt_sub_left_iff_add_lt
deleted
theorem
lt_sub_right_iff_add_lt
added
theorem
neg_add_le_iff_le_add'
deleted
theorem
neg_add_le_iff_le_add_right
added
theorem
neg_le_sub_iff_le_add'
deleted
theorem
neg_le_sub_iff_le_add_left
added
theorem
neg_lt_sub_iff_lt_add'
deleted
theorem
neg_lt_sub_iff_lt_add_left
added
theorem
sub_le_iff_le_add'
added
theorem
sub_le_iff_le_add
deleted
theorem
sub_left_le_iff_le_add
deleted
theorem
sub_left_lt_iff_lt_add
added
theorem
sub_lt_iff_lt_add'
added
theorem
sub_lt_iff_lt_add
deleted
theorem
sub_right_le_iff_le_add
deleted
theorem
sub_right_lt_iff_lt_add
Modified
analysis/ennreal.lean
Modified
analysis/limits.lean
Modified
analysis/measure_theory/lebesgue_measure.lean
Modified
analysis/measure_theory/measure_space.lean
Modified
analysis/metric_space.lean
added
theorem
abs_dist_sub_le
added
def
ball
added
theorem
ball_disjoint
added
theorem
ball_disjoint_same
added
theorem
ball_eq_empty_iff_nonpos
added
theorem
ball_half_subset
added
theorem
ball_mem_nhds
added
theorem
ball_subset
added
theorem
ball_subset_ball
added
theorem
cauchy_of_metric
added
theorem
continuous_of_metric
added
theorem
dist_eq_zero
deleted
theorem
dist_eq_zero_iff
added
theorem
dist_le_zero
deleted
theorem
dist_le_zero_iff
added
theorem
dist_mem_uniformity
added
theorem
dist_pos
deleted
theorem
dist_pos_of_ne
added
theorem
dist_triangle_left
added
theorem
dist_triangle_right
added
theorem
exists_ball_subset_ball
added
theorem
is_closed_ball
deleted
theorem
is_closed_closed_ball
added
theorem
is_open_ball
modified
theorem
is_open_metric
deleted
theorem
is_open_open_ball
added
theorem
mem_ball'
added
theorem
mem_ball
added
theorem
mem_ball_comm
added
theorem
mem_ball_self
added
theorem
mem_closed_ball
added
theorem
mem_nhds_iff_metric
deleted
theorem
mem_nhds_sets_iff_metric
deleted
theorem
mem_open_ball
added
def
metric_space.induced
added
theorem
metric_space.induced_uniform_embedding
added
def
metric_space.replace_uniformity
deleted
theorem
ne_of_dist_pos
modified
theorem
nhds_eq_metric
deleted
def
open_ball
deleted
theorem
open_ball_eq_empty_of_nonpos
deleted
theorem
open_ball_subset_open_ball_of_le
added
theorem
pos_of_mem_ball
deleted
theorem
pos_of_mem_open_ball
added
theorem
real.dist_eq
added
theorem
subtype.dist_eq
added
theorem
swap_dist
added
theorem
tendsto_nhds_of_metric
added
theorem
totally_bounded_of_metric
added
theorem
uniform_continuous_of_metric
added
theorem
uniform_embedding_of_metric
added
theorem
uniformity_dist_of_mem_uniformity
added
theorem
zero_eq_dist
deleted
theorem
zero_eq_dist_iff
Modified
analysis/real.lean
deleted
theorem
neg_preimage_closure
deleted
theorem
preimage_neg_real
added
theorem
real.neg_preimage_closure
deleted
theorem
tendsto_of_uniform_continuous_subtype
Modified
analysis/topology/continuity.lean
added
theorem
continuous.comp
added
theorem
continuous.prod_mk
added
theorem
continuous.tendsto
deleted
theorem
continuous_compose
deleted
theorem
continuous_eq_le_coinduced
added
theorem
continuous_iff_le_coinduced
deleted
theorem
continuous_iff_of_embedding
modified
theorem
continuous_inf_rng_left
modified
theorem
continuous_inf_rng_right
added
theorem
continuous_le_dom
added
theorem
continuous_le_rng
deleted
theorem
continuous_prod_mk
modified
theorem
continuous_sup_dom_left
modified
theorem
continuous_sup_dom_right
deleted
theorem
dense_embedding.closure_image_univ
added
theorem
dense_embedding.closure_range
modified
theorem
dense_embedding.inj_iff
added
theorem
dense_embedding.mk'
added
theorem
embedding.continuous_iff
added
theorem
embedding.tendsto_nhds_iff
modified
theorem
is_open_prod
deleted
theorem
tendsto_nhds_iff_of_embedding
Modified
analysis/topology/infinite_sum.lean
Modified
analysis/topology/topological_space.lean
added
theorem
mem_closure_iff
added
theorem
mem_closure_iff_nhds
Modified
analysis/topology/topological_structures.lean
added
theorem
filter.map_neg
added
theorem
induced_orderable_topology'
added
theorem
induced_orderable_topology
added
theorem
neg_preimage_closure
added
theorem
preimage_neg
added
theorem
uniform_add_group.mk'
Modified
analysis/topology/uniform_space.lean
added
theorem
Cauchy.mem_uniformity'
added
theorem
Cauchy.mem_uniformity
modified
theorem
Cauchy.pure_cauchy_dense
deleted
theorem
continuous_of_uniform
deleted
theorem
dense_embedding_of_uniform_embedding
added
theorem
id_rel_subset
added
theorem
le_nhds_lim_of_cauchy
added
theorem
mem_comp_rel
added
theorem
mem_id_rel
modified
theorem
mem_nhds_left
modified
theorem
mem_nhds_right
added
def
separated
added
theorem
separated_def'
added
theorem
separated_def
added
theorem
tendsto_of_uniform_continuous_subtype
added
theorem
totally_bounded_iff_subset
added
theorem
totally_bounded_preimage
added
theorem
uniform_continuous.comp
added
theorem
uniform_continuous.continuous
added
theorem
uniform_continuous.prod_mk
added
def
uniform_continuous
deleted
theorem
uniform_continuous_compose
added
theorem
uniform_continuous_def
deleted
theorem
uniform_continuous_of_embedding
deleted
theorem
uniform_continuous_prod_mk
added
theorem
uniform_embedding.dense_embedding
added
theorem
uniform_embedding.prod
added
theorem
uniform_embedding.uniform_continuous
added
theorem
uniform_embedding.uniform_continuous_iff
added
def
uniform_embedding
added
theorem
uniform_embedding_def'
added
theorem
uniform_embedding_def
deleted
theorem
uniform_embedding_prod
added
def
uniform_space.core.mk'
Modified
data/analysis/filter.lean
Modified
data/equiv.lean
Modified
data/fp/basic.lean
Modified
data/hash_map.lean
Modified
data/int/basic.lean
added
theorem
int.cast_injective
Modified
data/list/basic.lean
Modified
data/list/perm.lean
Modified
data/nat/cast.lean
added
theorem
nat.cast_injective
Modified
data/rat.lean
added
theorem
rat.cast_injective
Modified
data/real.lean
deleted
theorem
NEW.real.Inf_le
deleted
theorem
NEW.real.Sup_le
deleted
theorem
NEW.real.Sup_le_ub
deleted
theorem
NEW.real.add_lt_add_iff_left
deleted
theorem
NEW.real.ceil_add_int
deleted
theorem
NEW.real.ceil_coe
deleted
theorem
NEW.real.ceil_le
deleted
theorem
NEW.real.ceil_lt_add_one
deleted
theorem
NEW.real.ceil_mono
deleted
theorem
NEW.real.ceil_sub_int
deleted
theorem
NEW.real.exists_floor
deleted
theorem
NEW.real.exists_int_gt
deleted
theorem
NEW.real.exists_int_lt
deleted
theorem
NEW.real.exists_nat_gt
deleted
theorem
NEW.real.exists_pos_rat_lt
deleted
theorem
NEW.real.exists_rat_btwn
deleted
theorem
NEW.real.exists_rat_gt
deleted
theorem
NEW.real.exists_rat_lt
deleted
theorem
NEW.real.exists_rat_near'
deleted
theorem
NEW.real.exists_rat_near
deleted
theorem
NEW.real.exists_sup
deleted
theorem
NEW.real.floor_add_int
deleted
theorem
NEW.real.floor_coe
deleted
theorem
NEW.real.floor_le
deleted
theorem
NEW.real.floor_lt
deleted
theorem
NEW.real.floor_mono
deleted
theorem
NEW.real.floor_sub_int
deleted
theorem
NEW.real.inv_mk
deleted
theorem
NEW.real.inv_zero
deleted
theorem
NEW.real.lb_le_Inf
deleted
theorem
NEW.real.le_Inf
deleted
theorem
NEW.real.le_Sup
deleted
theorem
NEW.real.le_ceil
deleted
theorem
NEW.real.le_floor
deleted
theorem
NEW.real.le_mk_of_forall_le
deleted
theorem
NEW.real.lt_ceil
deleted
theorem
NEW.real.lt_floor_add_one
deleted
theorem
NEW.real.lt_succ_floor
deleted
def
NEW.real.mk
deleted
theorem
NEW.real.mk_add
deleted
theorem
NEW.real.mk_eq
deleted
theorem
NEW.real.mk_eq_mk
deleted
theorem
NEW.real.mk_eq_zero
deleted
theorem
NEW.real.mk_le
deleted
theorem
NEW.real.mk_le_of_forall_le
deleted
theorem
NEW.real.mk_lt
deleted
theorem
NEW.real.mk_mul
deleted
theorem
NEW.real.mk_neg
deleted
theorem
NEW.real.mk_pos
deleted
def
NEW.real.of_rat
deleted
theorem
NEW.real.of_rat_add
deleted
theorem
NEW.real.of_rat_eq_cast
deleted
theorem
NEW.real.of_rat_lt
deleted
theorem
NEW.real.of_rat_mul
deleted
theorem
NEW.real.of_rat_neg
deleted
theorem
NEW.real.of_rat_one
deleted
theorem
NEW.real.of_rat_sub
deleted
theorem
NEW.real.of_rat_zero
deleted
theorem
NEW.real.sub_one_lt_floor
deleted
def
NEW.real
added
theorem
cau_seq.abs_pos_of_not_lim_zero
added
theorem
cau_seq.add_apply
added
theorem
cau_seq.add_lim_zero
added
theorem
cau_seq.add_pos
added
theorem
cau_seq.bounded'
added
theorem
cau_seq.bounded
added
theorem
cau_seq.cauchy
added
theorem
cau_seq.cauchy₂
added
theorem
cau_seq.cauchy₃
added
def
cau_seq.const
added
theorem
cau_seq.const_add
added
theorem
cau_seq.const_apply
added
theorem
cau_seq.const_equiv
added
theorem
cau_seq.const_inj
added
theorem
cau_seq.const_le
added
theorem
cau_seq.const_lim_zero
added
theorem
cau_seq.const_lt
added
theorem
cau_seq.const_mul
added
theorem
cau_seq.const_neg
added
theorem
cau_seq.const_pos
added
theorem
cau_seq.const_sub
added
theorem
cau_seq.equiv_def₃
added
theorem
cau_seq.exists_gt
added
theorem
cau_seq.exists_lt
added
theorem
cau_seq.ext
added
def
cau_seq.inv
added
theorem
cau_seq.inv_apply
added
theorem
cau_seq.inv_aux
added
theorem
cau_seq.inv_mul_cancel
added
theorem
cau_seq.le_antisymm
added
theorem
cau_seq.le_total
added
def
cau_seq.lim_zero
added
theorem
cau_seq.lim_zero_congr
added
theorem
cau_seq.lt_irrefl
added
theorem
cau_seq.lt_of_eq_of_lt
added
theorem
cau_seq.lt_of_lt_of_eq
added
theorem
cau_seq.lt_total
added
theorem
cau_seq.lt_trans
added
def
cau_seq.mk_of_near
added
theorem
cau_seq.mk_of_near_equiv
added
theorem
cau_seq.mk_of_near_fun
added
theorem
cau_seq.mul_apply
added
theorem
cau_seq.mul_lim_zero
added
theorem
cau_seq.mul_pos
added
theorem
cau_seq.neg_apply
added
theorem
cau_seq.neg_lim_zero
added
theorem
cau_seq.not_lim_zero_of_pos
added
def
cau_seq.of_eq
added
theorem
cau_seq.one_apply
added
def
cau_seq.pos
added
theorem
cau_seq.pos_add_lim_zero
added
theorem
cau_seq.sub_apply
added
theorem
cau_seq.sub_lim_zero
added
theorem
cau_seq.trichotomy
added
theorem
cau_seq.zero_apply
added
theorem
cau_seq.zero_lim_zero
added
def
cau_seq
deleted
theorem
rat.cau_seq.abs_pos_of_not_lim_zero
deleted
theorem
rat.cau_seq.add_apply
deleted
theorem
rat.cau_seq.add_lim_zero
deleted
theorem
rat.cau_seq.add_pos
deleted
theorem
rat.cau_seq.bounded'
deleted
theorem
rat.cau_seq.bounded
deleted
theorem
rat.cau_seq.cauchy
deleted
theorem
rat.cau_seq.cauchy₂
deleted
theorem
rat.cau_seq.cauchy₃
deleted
theorem
rat.cau_seq.ext
deleted
def
rat.cau_seq.inv
deleted
theorem
rat.cau_seq.inv_apply
deleted
theorem
rat.cau_seq.inv_aux
deleted
theorem
rat.cau_seq.inv_mul_cancel
deleted
theorem
rat.cau_seq.le_antisymm
deleted
theorem
rat.cau_seq.le_total
deleted
def
rat.cau_seq.lim_zero
deleted
theorem
rat.cau_seq.lim_zero_congr
deleted
theorem
rat.cau_seq.lt_irrefl
deleted
theorem
rat.cau_seq.lt_of_eq_of_lt
deleted
theorem
rat.cau_seq.lt_of_lt_of_eq
deleted
theorem
rat.cau_seq.lt_trans
deleted
theorem
rat.cau_seq.mul_apply
deleted
theorem
rat.cau_seq.mul_lim_zero
deleted
theorem
rat.cau_seq.mul_pos
deleted
theorem
rat.cau_seq.neg_apply
deleted
theorem
rat.cau_seq.neg_lim_zero
deleted
theorem
rat.cau_seq.not_lim_zero_of_pos
deleted
def
rat.cau_seq.of_eq
deleted
def
rat.cau_seq.of_rat
deleted
theorem
rat.cau_seq.of_rat_add
deleted
theorem
rat.cau_seq.of_rat_apply
deleted
theorem
rat.cau_seq.of_rat_lim_zero
deleted
theorem
rat.cau_seq.of_rat_mul
deleted
theorem
rat.cau_seq.of_rat_neg
deleted
theorem
rat.cau_seq.of_rat_pos
deleted
theorem
rat.cau_seq.of_rat_sub
deleted
theorem
rat.cau_seq.one_apply
deleted
def
rat.cau_seq.pos
deleted
theorem
rat.cau_seq.pos_add_lim_zero
deleted
theorem
rat.cau_seq.sub_apply
deleted
theorem
rat.cau_seq.sub_lim_zero
deleted
theorem
rat.cau_seq.trichotomy
deleted
theorem
rat.cau_seq.zero_apply
deleted
theorem
rat.cau_seq.zero_lim_zero
deleted
def
rat.cau_seq
added
theorem
rat_add_continuous_lemma
added
theorem
rat_inv_continuous_lemma
added
theorem
rat_mul_continuous_lemma
added
theorem
real.Inf_le
added
theorem
real.Inf_lt
added
theorem
real.Sup_le
added
theorem
real.Sup_le_ub
added
theorem
real.add_lt_add_iff_left
added
theorem
real.cau_seq_converges
added
theorem
real.ceil_add_int
added
theorem
real.ceil_coe
added
theorem
real.ceil_le
added
theorem
real.ceil_lt_add_one
added
theorem
real.ceil_mono
added
theorem
real.ceil_sub_int
added
theorem
real.equiv_lim
added
theorem
real.exists_floor
added
theorem
real.exists_int_gt
added
theorem
real.exists_int_lt
added
theorem
real.exists_nat_gt
added
theorem
real.exists_pos_rat_lt
added
theorem
real.exists_rat_btwn
added
theorem
real.exists_rat_gt
added
theorem
real.exists_rat_lt
added
theorem
real.exists_rat_near'
added
theorem
real.exists_rat_near
added
theorem
real.exists_sup
added
theorem
real.floor_add_int
added
theorem
real.floor_coe
added
theorem
real.floor_le
added
theorem
real.floor_lt
added
theorem
real.floor_mono
added
theorem
real.floor_nonneg
added
theorem
real.floor_sub_int
added
theorem
real.inv_mk
added
theorem
real.inv_zero
added
theorem
real.lb_le_Inf
added
theorem
real.le_Inf
added
theorem
real.le_Sup
added
theorem
real.le_ceil
added
theorem
real.le_floor
added
theorem
real.le_mk_of_forall_le
added
theorem
real.lt_Sup
added
theorem
real.lt_ceil
added
theorem
real.lt_floor_add_one
added
theorem
real.lt_succ_floor
added
def
real.mk
added
theorem
real.mk_add
added
theorem
real.mk_eq
added
theorem
real.mk_eq_mk
added
theorem
real.mk_eq_zero
added
theorem
real.mk_le
added
theorem
real.mk_le_of_forall_le
added
theorem
real.mk_lt
added
theorem
real.mk_mul
added
theorem
real.mk_neg
added
theorem
real.mk_pos
added
def
real.of_rat
added
theorem
real.of_rat_add
added
theorem
real.of_rat_eq_cast
added
theorem
real.of_rat_lt
added
theorem
real.of_rat_mul
added
theorem
real.of_rat_neg
added
theorem
real.of_rat_one
added
theorem
real.of_rat_sub
added
theorem
real.of_rat_zero
added
theorem
real.sub_one_lt_floor
added
def
real
Modified
data/set/basic.lean
added
theorem
set.image_preimage_eq_inter_range
deleted
theorem
set.image_preimage_eq_inter_rng
added
theorem
set.image_univ
modified
theorem
set.mem_range
modified
theorem
set.preimage_image_eq
added
theorem
set.prod_range_range_eq
deleted
theorem
set.quot_mk_image_univ_eq
added
theorem
set.quot_mk_range_eq
added
theorem
set.range_comp
deleted
theorem
set.range_compose
deleted
theorem
set.range_eq_image
added
theorem
set.range_subset_iff
Modified
data/set/finite.lean
added
theorem
set.finite_preimage
Modified
data/set/lattice.lean
modified
theorem
set.Inter_eq_sInter_image
modified
theorem
set.Union_eq_sUnion_image
added
theorem
set.bInter_subset_bInter_left
added
theorem
set.bUnion_subset_bUnion_left
added
theorem
set.subtype_val_range
Modified
logic/basic.lean
added
def
Exists.imp
deleted
theorem
exists_of_exists
deleted
theorem
forall_of_forall
Modified
logic/function.lean
added
theorem
function.bijective_iff_has_inverse
added
theorem
function.injective_iff_has_left_inverse
added
theorem
function.left_inverse_surj_inv
added
theorem
function.surjective_iff_has_right_inverse
Modified
order/filter.lean
added
theorem
filter.filter.ext
added
theorem
filter.filter_eq_iff
added
theorem
filter.le_def
added
theorem
filter.mem_Sup_sets
deleted
theorem
filter.mem_at_top_iff
added
theorem
filter.mem_at_top_sets
modified
theorem
filter.mem_bind_sets
deleted
theorem
filter.mem_lift'_iff
added
theorem
filter.mem_lift'_sets
deleted
theorem
filter.mem_lift_iff
added
theorem
filter.mem_lift_sets
modified
theorem
filter.mem_map
added
theorem
filter.mem_principal_self
modified
theorem
filter.mem_principal_sets
deleted
theorem
filter.mem_prod_iff
added
theorem
filter.mem_prod_sets
added
theorem
filter.mem_pure_sets
modified
theorem
filter.mem_return_sets
added
theorem
filter.mem_supr_sets
deleted
theorem
filter.mem_vmap
added
theorem
filter.mem_vmap_sets
modified
theorem
filter.monotone_map
modified
theorem
filter.monotone_vmap
added
theorem
filter.pure_neq_bot
deleted
theorem
filter.return_neq_bot
added
theorem
filter.tendsto.comp
added
theorem
filter.tendsto.prod_mk
deleted
theorem
filter.tendsto_compose
added
theorem
filter.tendsto_def
added
theorem
filter.tendsto_iff_vmap
modified
theorem
filter.tendsto_inf
deleted
theorem
filter.tendsto_inf_left
modified
theorem
filter.tendsto_infi'
modified
theorem
filter.tendsto_infi
added
theorem
filter.tendsto_le_left
added
theorem
filter.tendsto_le_right
modified
theorem
filter.tendsto_principal
modified
theorem
filter.tendsto_principal_principal
deleted
theorem
filter.tendsto_prod_mk
Modified
order/galois_connection.lean