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