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

added theorem div_le_iff'
added theorem div_lt_iff'
added theorem le_div_iff'
added theorem lt_div_iff'
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'
added theorem neg_le_sub_iff_le_add'
added theorem neg_lt_sub_iff_lt_add'
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
added theorem abs_dist_sub_le
added def ball
added theorem ball_disjoint
added theorem ball_disjoint_same
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 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
deleted theorem ne_of_dist_pos
modified theorem nhds_eq_metric
deleted def open_ball
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 zero_eq_dist
deleted theorem zero_eq_dist_iff
added theorem continuous.comp
added theorem continuous.prod_mk
added theorem continuous.tendsto
deleted theorem continuous_compose
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
modified theorem dense_embedding.inj_iff
added theorem dense_embedding.mk'
modified theorem is_open_prod
deleted theorem NEW.real.Inf_le
deleted theorem NEW.real.Sup_le
deleted theorem NEW.real.Sup_le_ub
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_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.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_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.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 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 def cau_seq.of_eq
added theorem cau_seq.one_apply
added def cau_seq.pos
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.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.le_antisymm
deleted theorem rat.cau_seq.le_total
deleted theorem rat.cau_seq.lt_irrefl
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 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_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.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 real.Inf_le
added theorem real.Inf_lt
added theorem real.Sup_le
added theorem real.Sup_le_ub
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.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_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
added theorem set.image_univ
modified theorem set.mem_range
modified theorem set.preimage_image_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
added def Exists.imp
deleted theorem exists_of_exists
deleted theorem forall_of_forall
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
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
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
modified theorem filter.tendsto_principal
deleted theorem filter.tendsto_prod_mk