Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-19 02:24 04094c4b

View on Github →

feat(analysis/box_integral): Divergence thm for a Henstock-style integral (#9496)

Define integrals of Riemann, McShane, and Henstock (plus a few variations).
Prove basic properties.
Prove a version of the divergence theorem for one of these integrals.
Prove that a Bochner integrable function is McShane integrable.

Estimated changes

Modified docs/references.bib

Modified src/algebra/order/field.lean

added theorem add_div_two_lt_right

added theorem exists_pos_mul_lt

added theorem left_lt_add_div_two

Created src/analysis/box_integral/basic.lean

added theorem box_integral.has_integral.add

added theorem box_integral.has_integral.integrable

added theorem box_integral.has_integral.integral_eq

added theorem box_integral.has_integral.mono

added theorem box_integral.has_integral.neg

added theorem box_integral.has_integral.smul

added theorem box_integral.has_integral.sub

added theorem box_integral.has_integral.tendsto

added theorem box_integral.has_integral.unique

added def box_integral.has_integral

added theorem box_integral.has_integral_McShane_of_forall_is_o

added theorem box_integral.has_integral_const

added theorem box_integral.has_integral_iff

added theorem box_integral.has_integral_of_bRiemann_eq_ff_of_forall_is_o

added theorem box_integral.has_integral_of_le_Henstock_of_forall_is_o

added theorem box_integral.has_integral_of_mul

added theorem box_integral.has_integral_sum

added theorem box_integral.has_integral_zero

added theorem box_integral.integrable.add

added theorem box_integral.integrable.cauchy_map_integral_sum_to_filter_Union

added def box_integral.integrable.convergence_r

added theorem box_integral.integrable.convergence_r_cond

added theorem box_integral.integrable.dist_integral_sum_integral_le_of_mem_base_set

added theorem box_integral.integrable.dist_integral_sum_le_of_mem_base_set

added theorem box_integral.integrable.dist_integral_sum_sum_integral_le_of_mem_base_set

added theorem box_integral.integrable.dist_integral_sum_sum_integral_le_of_mem_base_set_of_Union_eq

added theorem box_integral.integrable.mono

added theorem box_integral.integrable.neg

added theorem box_integral.integrable.of_neg

added theorem box_integral.integrable.of_smul

added theorem box_integral.integrable.smul

added theorem box_integral.integrable.sub

added theorem box_integral.integrable.sum_integral_congr

added theorem box_integral.integrable.tendsto_integral_sum_sum_integral

added theorem box_integral.integrable.tendsto_integral_sum_to_filter_Union_single

added theorem box_integral.integrable.tendsto_integral_sum_to_filter_prod_self_inf_Union_eq_uniformity

added def box_integral.integrable.to_box_additive

added theorem box_integral.integrable.to_subbox

added theorem box_integral.integrable.to_subbox_aux

added def box_integral.integrable

added theorem box_integral.integrable_const

added theorem box_integral.integrable_iff_cauchy

added theorem box_integral.integrable_iff_cauchy_basis

added theorem box_integral.integrable_neg

added theorem box_integral.integrable_of_continuous_on

added theorem box_integral.integrable_zero

added def box_integral.integral

added theorem box_integral.integral_add

added theorem box_integral.integral_const

added theorem box_integral.integral_neg

added theorem box_integral.integral_nonneg

added theorem box_integral.integral_smul

added theorem box_integral.integral_sub

added def box_integral.integral_sum

added theorem box_integral.integral_sum_add

added theorem box_integral.integral_sum_bUnion_partition

added theorem box_integral.integral_sum_bUnion_tagged

added theorem box_integral.integral_sum_disj_union

added theorem box_integral.integral_sum_fiberwise

added theorem box_integral.integral_sum_inf_partition

added theorem box_integral.integral_sum_neg

added theorem box_integral.integral_sum_smul

added theorem box_integral.integral_sum_sub_partitions

added theorem box_integral.integral_zero

added theorem box_integral.norm_integral_le_of_le_const

added theorem box_integral.norm_integral_le_of_norm_le

Created src/analysis/box_integral/box/basic.lean

added theorem box_integral.box.Icc_def

added theorem box_integral.box.Icc_eq_pi

added theorem box_integral.box.antitone_lower

added theorem box_integral.box.bUnion_coe_eq_coe

added theorem box_integral.box.coe_bot

added theorem box_integral.box.coe_coe

added theorem box_integral.box.coe_eq_pi

added theorem box_integral.box.coe_inf

added theorem box_integral.box.coe_inj

added theorem box_integral.box.coe_mk'

added theorem box_integral.box.coe_ne_empty

added theorem box_integral.box.coe_subset_Icc

added theorem box_integral.box.coe_subset_coe

added theorem box_integral.box.continuous_on_face_Icc

added theorem box_integral.box.diam_Icc_le_of_distortion_le

added theorem box_integral.box.disjoint_coe

added theorem box_integral.box.disjoint_with_bot_coe

added theorem box_integral.box.dist_le_distortion_mul

added def box_integral.box.distortion

added theorem box_integral.box.distortion_eq_of_sub_eq_div

added theorem box_integral.box.empty_ne_coe

added theorem box_integral.box.exists_mem

added theorem box_integral.box.ext

added def box_integral.box.face

added theorem box_integral.box.face_mk

added theorem box_integral.box.face_mono

added theorem box_integral.box.injective_coe

added theorem box_integral.box.is_some_iff

added theorem box_integral.box.le_def

added theorem box_integral.box.le_iff_Icc

added theorem box_integral.box.le_iff_bounds

added theorem box_integral.box.le_tfae

added theorem box_integral.box.lower_le_upper

added theorem box_integral.box.lower_mem_Icc

added theorem box_integral.box.maps_to_insert_nth_face

added theorem box_integral.box.maps_to_insert_nth_face_Icc

added theorem box_integral.box.mem_coe

added theorem box_integral.box.mem_def

added theorem box_integral.box.mem_mk

added theorem box_integral.box.mem_univ_Ioc

added def box_integral.box.mk'

added theorem box_integral.box.mk'_eq_bot

added theorem box_integral.box.mk'_eq_coe

added theorem box_integral.box.monotone_upper

added theorem box_integral.box.ne_of_disjoint_coe

added theorem box_integral.box.nndist_le_distortion_mul

added theorem box_integral.box.nonempty_coe

added theorem box_integral.box.not_disjoint_coe_iff_nonempty_inter

added theorem box_integral.box.upper_mem

added theorem box_integral.box.upper_mem_Icc

added theorem box_integral.box.with_bot_coe_inj

added theorem box_integral.box.with_bot_coe_subset_iff

added structure box_integral.box

Created src/analysis/box_integral/box/subbox_induction.lean

added theorem box_integral.box.Union_coe_split_center_box

added theorem box_integral.box.disjoint_split_center_box

added theorem box_integral.box.exists_mem_split_center_box

added theorem box_integral.box.injective_split_center_box

added theorem box_integral.box.mem_split_center_box

added def box_integral.box.split_center_box

added def box_integral.box.split_center_box_emb

added theorem box_integral.box.split_center_box_le

added theorem box_integral.box.subbox_induction_on'

added theorem box_integral.box.upper_sub_lower_split_center_box

Created src/analysis/box_integral/divergence_theorem.lean

added theorem box_integral.has_integral_bot_divergence_of_forall_has_deriv_within_at

added theorem box_integral.has_integral_bot_pderiv

added theorem box_integral.norm_volume_sub_integral_face_upper_sub_lower_smul_le

Created src/analysis/box_integral/integrability.lean

added theorem box_integral.has_integral.congr_ae

added theorem box_integral.has_integral_indicator_const

added theorem box_integral.has_integral_zero_of_ae_eq_zero

added theorem measure_theory.integrable_on.has_box_integral

added theorem measure_theory.simple_func.box_integral_eq_integral

added theorem measure_theory.simple_func.has_box_integral

Created src/analysis/box_integral/partition/additive.lean

added theorem box_integral.box_additive_map.coe_inj

added theorem box_integral.box_additive_map.coe_injective

added theorem box_integral.box_additive_map.coe_mk

added def box_integral.box_additive_map.map

added theorem box_integral.box_additive_map.map_split_add

added def box_integral.box_additive_map.of_map_split_add

added def box_integral.box_additive_map.restrict

added theorem box_integral.box_additive_map.sum_boxes_congr

added theorem box_integral.box_additive_map.sum_partition_boxes

added theorem box_integral.box_additive_map.to_fun_eq_coe

added def box_integral.box_additive_map.to_smul

added theorem box_integral.box_additive_map.to_smul_apply

added def box_integral.box_additive_map.{u}

added structure box_integral.box_additive_map

Created src/analysis/box_integral/partition/basic.lean

added theorem box_integral.prepartition.Union_bUnion

added theorem box_integral.prepartition.Union_bUnion_partition

added theorem box_integral.prepartition.Union_bot

added theorem box_integral.prepartition.Union_def'

added theorem box_integral.prepartition.Union_def

added theorem box_integral.prepartition.Union_disj_union

added theorem box_integral.prepartition.Union_eq_empty

added theorem box_integral.prepartition.Union_filter_not

added theorem box_integral.prepartition.Union_inf

added theorem box_integral.prepartition.Union_mono

added theorem box_integral.prepartition.Union_of_with_bot

added theorem box_integral.prepartition.Union_restrict

added theorem box_integral.prepartition.Union_single

added theorem box_integral.prepartition.Union_subset

added theorem box_integral.prepartition.Union_top

added def box_integral.prepartition.bUnion

added theorem box_integral.prepartition.bUnion_assoc

added theorem box_integral.prepartition.bUnion_congr

added theorem box_integral.prepartition.bUnion_congr_of_le

added def box_integral.prepartition.bUnion_index

added theorem box_integral.prepartition.bUnion_index_le

added theorem box_integral.prepartition.bUnion_index_mem

added theorem box_integral.prepartition.bUnion_index_of_mem

added theorem box_integral.prepartition.bUnion_le

added theorem box_integral.prepartition.bUnion_le_iff

added theorem box_integral.prepartition.bUnion_top

added theorem box_integral.prepartition.bot_boxes

added theorem box_integral.prepartition.card_filter_mem_Icc_le

added def box_integral.prepartition.disj_union

added theorem box_integral.prepartition.disjoint_boxes_of_disjoint_Union

added theorem box_integral.prepartition.disjoint_coe_of_mem

added def box_integral.prepartition.distortion

added theorem box_integral.prepartition.distortion_bUnion

added theorem box_integral.prepartition.distortion_bot

added theorem box_integral.prepartition.distortion_disj_union

added theorem box_integral.prepartition.distortion_le_iff

added theorem box_integral.prepartition.distortion_le_of_mem

added theorem box_integral.prepartition.distortion_of_const

added theorem box_integral.prepartition.distortion_top

added theorem box_integral.prepartition.eq_of_boxes_subset_Union_superset

added theorem box_integral.prepartition.eq_of_le

added theorem box_integral.prepartition.eq_of_le_of_le

added theorem box_integral.prepartition.eq_of_mem_of_mem

added theorem box_integral.prepartition.ext

added def box_integral.prepartition.filter

added theorem box_integral.prepartition.filter_le

added theorem box_integral.prepartition.filter_of_true

added theorem box_integral.prepartition.filter_true

added theorem box_integral.prepartition.inf_def

added theorem box_integral.prepartition.inj_on_set_of_mem_Icc_set_of_lower_eq

added theorem box_integral.prepartition.injective_boxes

added theorem box_integral.prepartition.is_partition.Union_eq

added theorem box_integral.prepartition.is_partition.Union_subset

added theorem box_integral.prepartition.is_partition.eq_of_boxes_subset

added theorem box_integral.prepartition.is_partition.le_iff

added theorem box_integral.prepartition.is_partition.nonempty_boxes

added def box_integral.prepartition.is_partition

added theorem box_integral.prepartition.is_partition_disj_union_of_eq_diff

added theorem box_integral.prepartition.is_partition_iff_Union_eq

added theorem box_integral.prepartition.is_partition_single_iff

added theorem box_integral.prepartition.is_partition_top

added theorem box_integral.prepartition.le_bUnion_iff

added theorem box_integral.prepartition.le_bUnion_index

added theorem box_integral.prepartition.le_def

added theorem box_integral.prepartition.le_iff_nonempty_imp_le_and_Union_subset

added theorem box_integral.prepartition.le_of_mem

added theorem box_integral.prepartition.le_of_with_bot

added theorem box_integral.prepartition.lower_le_lower

added theorem box_integral.prepartition.mem_Union

added theorem box_integral.prepartition.mem_bUnion

added theorem box_integral.prepartition.mem_bUnion_index

added theorem box_integral.prepartition.mem_boxes

added theorem box_integral.prepartition.mem_disj_union

added theorem box_integral.prepartition.mem_filter

added theorem box_integral.prepartition.mem_inf

added theorem box_integral.prepartition.mem_mk

added theorem box_integral.prepartition.mem_of_with_bot

added theorem box_integral.prepartition.mem_restrict'

added theorem box_integral.prepartition.mem_restrict

added theorem box_integral.prepartition.mem_single

added theorem box_integral.prepartition.mem_top

added theorem box_integral.prepartition.monotone_restrict

added theorem box_integral.prepartition.not_mem_bot

added def box_integral.prepartition.of_with_bot

added theorem box_integral.prepartition.of_with_bot_le

added theorem box_integral.prepartition.of_with_bot_mono

added def box_integral.prepartition.restrict

added theorem box_integral.prepartition.restrict_bUnion

added theorem box_integral.prepartition.restrict_boxes_of_le

added theorem box_integral.prepartition.restrict_mono

added theorem box_integral.prepartition.restrict_self

added def box_integral.prepartition.single

added theorem box_integral.prepartition.subset_Union

added theorem box_integral.prepartition.sum_bUnion_boxes

added theorem box_integral.prepartition.sum_disj_union_boxes

added theorem box_integral.prepartition.sum_fiberwise

added theorem box_integral.prepartition.sum_of_with_bot

added theorem box_integral.prepartition.top_boxes

added theorem box_integral.prepartition.upper_le_upper

added structure box_integral.prepartition

Created src/analysis/box_integral/partition/filter.lean

added def box_integral.integration_params.Henstock

added theorem box_integral.integration_params.Henstock_le_McShane

added theorem box_integral.integration_params.Henstock_le_Riemann

added def box_integral.integration_params.McShane

added def box_integral.integration_params.Riemann

added theorem box_integral.integration_params.bUnion_tagged_mem_base_set

added def box_integral.integration_params.equiv_prod

added theorem box_integral.integration_params.eventually_is_partition

added theorem box_integral.integration_params.exists_mem_base_set_is_partition

added theorem box_integral.integration_params.exists_mem_base_set_le_Union_eq

added theorem box_integral.integration_params.has_basis_to_filter

added theorem box_integral.integration_params.has_basis_to_filter_Union

added theorem box_integral.integration_params.has_basis_to_filter_Union_top

added theorem box_integral.integration_params.has_basis_to_filter_distortion

added theorem box_integral.integration_params.has_basis_to_filter_distortion_Union

added def box_integral.integration_params.iso_prod

added theorem box_integral.integration_params.mem_base_set.exists_common_compl

added theorem box_integral.integration_params.mem_base_set.mono'

added theorem box_integral.integration_params.mem_base_set.mono

added structure box_integral.integration_params.mem_base_set

added theorem box_integral.integration_params.r_cond.min

added theorem box_integral.integration_params.r_cond.mono

added def box_integral.integration_params.r_cond

added theorem box_integral.integration_params.r_cond_of_bRiemann_eq_ff

added theorem box_integral.integration_params.tendsto_embed_box_to_filter_Union_top

added def box_integral.integration_params.to_filter

added def box_integral.integration_params.to_filter_Union

added theorem box_integral.integration_params.to_filter_Union_congr

added theorem box_integral.integration_params.to_filter_Union_mono

added def box_integral.integration_params.to_filter_distortion

added def box_integral.integration_params.to_filter_distortion_Union

added theorem box_integral.integration_params.to_filter_distortion_Union_ne_bot

added theorem box_integral.integration_params.to_filter_distortion_mono

added theorem box_integral.integration_params.to_filter_inf_Union_eq

added theorem box_integral.integration_params.to_filter_mono

added structure box_integral.integration_params

Created src/analysis/box_integral/partition/measure.lean

added theorem box_integral.box.measurable_set_Icc

added theorem box_integral.box.measurable_set_coe

added theorem box_integral.box.measure_Icc_lt_top

added theorem box_integral.box.measure_coe_lt_top

added theorem box_integral.box.volume_apply

added theorem box_integral.box.volume_face_mul

added theorem box_integral.box_additive_map.volume_apply

added theorem box_integral.prepartition.measure_Union_to_real

added def measure_theory.measure.to_box_additive

Created src/analysis/box_integral/partition/split.lean

added theorem box_integral.box.coe_split_lower

added theorem box_integral.box.coe_split_upper

added theorem box_integral.box.disjoint_split_lower_split_upper

added def box_integral.box.split_lower

added theorem box_integral.box.split_lower_def

added theorem box_integral.box.split_lower_eq_bot

added theorem box_integral.box.split_lower_eq_self

added theorem box_integral.box.split_lower_le

added theorem box_integral.box.split_lower_ne_split_upper

added def box_integral.box.split_upper

added theorem box_integral.box.split_upper_def

added theorem box_integral.box.split_upper_eq_bot

added theorem box_integral.box.split_upper_eq_self

added theorem box_integral.box.split_upper_le

added theorem box_integral.prepartition.Union_compl

added theorem box_integral.prepartition.Union_split

added theorem box_integral.prepartition.Union_split_many

added theorem box_integral.prepartition.coe_eq_of_mem_split_of_lt_mem

added theorem box_integral.prepartition.coe_eq_of_mem_split_of_mem_le

added def box_integral.prepartition.compl

added theorem box_integral.prepartition.compl_congr

added theorem box_integral.prepartition.compl_top

added theorem box_integral.prepartition.eventually_not_disjoint_imp_le_of_mem_split_many

added theorem box_integral.prepartition.eventually_split_many_inf_eq_filter

added theorem box_integral.prepartition.exists_Union_eq_diff

added theorem box_integral.prepartition.exists_split_many_inf_eq_filter_of_finite

added theorem box_integral.prepartition.inf_split

added theorem box_integral.prepartition.inf_split_many

added theorem box_integral.prepartition.is_partition.compl_eq_bot

added theorem box_integral.prepartition.is_partition.exists_split_many_le

added theorem box_integral.prepartition.is_partition_split

added theorem box_integral.prepartition.is_partition_split_many

added theorem box_integral.prepartition.mem_split_iff'

added theorem box_integral.prepartition.mem_split_iff

added theorem box_integral.prepartition.not_disjoint_imp_le_of_subset_of_mem_split_many

added theorem box_integral.prepartition.restrict_split

added def box_integral.prepartition.split

added def box_integral.prepartition.split_many

added theorem box_integral.prepartition.split_many_empty

added theorem box_integral.prepartition.split_many_insert

added theorem box_integral.prepartition.split_many_le_split

added theorem box_integral.prepartition.split_of_not_mem_Ioo

added theorem box_integral.prepartition.sum_split_boxes

Created src/analysis/box_integral/partition/subbox_induction.lean

added theorem box_integral.box.exists_tagged_partition_is_Henstock_is_subordinate_homothetic

added theorem box_integral.box.subbox_induction_on

added theorem box_integral.prepartition.Union_to_subordinate

added theorem box_integral.prepartition.distortion_to_subordinate

added theorem box_integral.prepartition.exists_tagged_le_is_Henstock_is_subordinate_Union_eq

added theorem box_integral.prepartition.is_Henstock_to_subordinate

added theorem box_integral.prepartition.is_partition_split_center

added theorem box_integral.prepartition.is_subordinate_to_subordinate

added theorem box_integral.prepartition.mem_split_center

added def box_integral.prepartition.split_center

added def box_integral.prepartition.to_subordinate

added theorem box_integral.prepartition.to_subordinate_to_prepartition_le

added theorem box_integral.prepartition.upper_sub_lower_of_mem_split_center

added theorem box_integral.tagged_prepartition.Union_union_compl_to_subordinate_boxes

added theorem box_integral.tagged_prepartition.distortion_union_compl_to_subordinate

added theorem box_integral.tagged_prepartition.is_partition_union_compl_to_subordinate

added def box_integral.tagged_prepartition.union_compl_to_subordinate

added theorem box_integral.tagged_prepartition.union_compl_to_subordinate_boxes

Created src/analysis/box_integral/partition/tagged.lean

added theorem box_integral.prepartition.Union_bUnion_tagged

added def box_integral.prepartition.bUnion_tagged

added theorem box_integral.prepartition.distortion_bUnion_tagged

added theorem box_integral.prepartition.forall_bUnion_tagged

added theorem box_integral.prepartition.is_partition.bUnion_tagged

added theorem box_integral.prepartition.mem_bUnion_tagged

added theorem box_integral.prepartition.tag_bUnion_tagged

added def box_integral.tagged_prepartition.Union

added theorem box_integral.tagged_prepartition.Union_def

added theorem box_integral.tagged_prepartition.Union_disj_union

added theorem box_integral.tagged_prepartition.Union_filter_not

added theorem box_integral.tagged_prepartition.Union_mk

added theorem box_integral.tagged_prepartition.Union_single

added theorem box_integral.tagged_prepartition.Union_subset

added theorem box_integral.tagged_prepartition.Union_to_prepartition

added def box_integral.tagged_prepartition.bUnion_prepartition

added def box_integral.tagged_prepartition.disj_union

added theorem box_integral.tagged_prepartition.disj_union_boxes

added theorem box_integral.tagged_prepartition.disj_union_tag_of_mem_left

added theorem box_integral.tagged_prepartition.disj_union_tag_of_mem_right

added def box_integral.tagged_prepartition.distortion

added theorem box_integral.tagged_prepartition.distortion_bUnion_prepartition

added theorem box_integral.tagged_prepartition.distortion_disj_union

added theorem box_integral.tagged_prepartition.distortion_filter_le

added theorem box_integral.tagged_prepartition.distortion_le_iff

added theorem box_integral.tagged_prepartition.distortion_le_of_mem

added theorem box_integral.tagged_prepartition.distortion_of_const

added theorem box_integral.tagged_prepartition.distortion_single

added def box_integral.tagged_prepartition.embed_box

added def box_integral.tagged_prepartition.filter

added theorem box_integral.tagged_prepartition.forall_mem_single

added def box_integral.tagged_prepartition.inf_prepartition

added theorem box_integral.tagged_prepartition.inf_prepartition_to_prepartition

added theorem box_integral.tagged_prepartition.is_Henstock.card_filter_tag_eq_le

added theorem box_integral.tagged_prepartition.is_Henstock.disj_union

added def box_integral.tagged_prepartition.is_Henstock

added theorem box_integral.tagged_prepartition.is_Henstock_bUnion_tagged

added theorem box_integral.tagged_prepartition.is_Henstock_single

added theorem box_integral.tagged_prepartition.is_Henstock_single_iff

added theorem box_integral.tagged_prepartition.is_partition.bUnion_prepartition

added theorem box_integral.tagged_prepartition.is_partition.inf_prepartition

added def box_integral.tagged_prepartition.is_partition

added theorem box_integral.tagged_prepartition.is_partition_iff_Union_eq

added theorem box_integral.tagged_prepartition.is_partition_single

added theorem box_integral.tagged_prepartition.is_partition_single_iff

added theorem box_integral.tagged_prepartition.is_subordinate.bUnion_prepartition

added theorem box_integral.tagged_prepartition.is_subordinate.diam_le

added theorem box_integral.tagged_prepartition.is_subordinate.disj_union

added theorem box_integral.tagged_prepartition.is_subordinate.inf_prepartition

added theorem box_integral.tagged_prepartition.is_subordinate.mono'

added theorem box_integral.tagged_prepartition.is_subordinate.mono

added def box_integral.tagged_prepartition.is_subordinate

added theorem box_integral.tagged_prepartition.is_subordinate_bUnion_tagged

added theorem box_integral.tagged_prepartition.is_subordinate_single

added theorem box_integral.tagged_prepartition.mem_Union

added theorem box_integral.tagged_prepartition.mem_disj_union

added theorem box_integral.tagged_prepartition.mem_filter

added theorem box_integral.tagged_prepartition.mem_inf_prepartition_comm

added theorem box_integral.tagged_prepartition.mem_mk

added theorem box_integral.tagged_prepartition.mem_single

added theorem box_integral.tagged_prepartition.mem_to_prepartition

added def box_integral.tagged_prepartition.single

added theorem box_integral.tagged_prepartition.subset_Union

added structure box_integral.tagged_prepartition

Modified src/data/set/lattice.lean

added theorem set.bUnion_diff_bUnion_eq

added theorem set.bUnion_diff_bUnion_subset

Modified src/logic/function/basic.lean

added theorem function.exists_update_iff

Modified src/topology/metric_space/basic.lean

added theorem real.dist_le_of_mem_pi_Icc