Commit 2023-03-03 17:48 800a22ac

View on Github →

feat: port Topology.MetricSpace.Basic (#2425)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/MetricSpace/Basic.lean

added def Bornology.ofDist

added theorem CauchySeq.bounded_range

added theorem ContinuousOn.isSeparable_image

added theorem Dense.exists_dist_lt

added def EMetricSpace.toMetricSpace

added def EMetricSpace.toMetricSpaceOfDist

added def Embedding.comapMetricSpace

added theorem Filter.Tendsto.congr_dist

added theorem Fin.dist_insertNth_insertNth

added theorem Fin.nndist_insertNth_insertNth

added def Inducing.comapPseudoMetricSpace

added theorem IsCompact.bounded

added theorem IsCompact.isSeparable

added theorem IsComplete.nonempty_interᵢ_of_nonempty_bInter

added theorem Metric.Bounded.ediam_ne_top

added theorem Metric.Bounded.isCompact_closure

added theorem Metric.Bounded.mono

added theorem Metric.Bounded.subset_ball

added theorem Metric.Bounded.subset_ball_lt

added theorem Metric.Bounded.union

added def Metric.Bounded

added def Metric.ball

added theorem Metric.ball_disjoint_ball

added theorem Metric.ball_disjoint_closedBall

added theorem Metric.ball_eq_ball'

added theorem Metric.ball_eq_ball

added theorem Metric.ball_eq_empty

added theorem Metric.ball_half_subset

added theorem Metric.ball_mem_nhds

added theorem Metric.ball_subset

added theorem Metric.ball_subset_ball'

added theorem Metric.ball_subset_ball

added theorem Metric.ball_subset_closedBall

added theorem Metric.ball_subset_interior_closedBall

added theorem Metric.ball_union_sphere

added theorem Metric.ball_zero

added theorem Metric.bounded_Icc

added theorem Metric.bounded_Ico

added theorem Metric.bounded_Ioc

added theorem Metric.bounded_Ioo

added theorem Metric.bounded_ball

added theorem Metric.bounded_bunionᵢ

added theorem Metric.bounded_closedBall

added theorem Metric.bounded_closure_iff

added theorem Metric.bounded_closure_of_bounded

added theorem Metric.bounded_empty

added theorem Metric.bounded_iff_ediam_ne_top

added theorem Metric.bounded_iff_isBounded

added theorem Metric.bounded_iff_mem_bounded

added theorem Metric.bounded_iff_subset_ball

added theorem Metric.bounded_of_bddAbove_of_bddBelow

added theorem Metric.bounded_of_compactSpace

added theorem Metric.bounded_of_finite

added theorem Metric.bounded_range_iff

added theorem Metric.bounded_range_of_cauchy_map_cofinite

added theorem Metric.bounded_range_of_tendsto

added theorem Metric.bounded_range_of_tendsto_cofinite

added theorem Metric.bounded_range_of_tendsto_cofinite_uniformity

added theorem Metric.bounded_singleton

added theorem Metric.bounded_sphere

added theorem Metric.bounded_union

added theorem Metric.cauchySeq_iff'

added theorem Metric.cauchySeq_iff

added def Metric.closedBall

added theorem Metric.closedBall_diff_ball

added theorem Metric.closedBall_diff_sphere

added theorem Metric.closedBall_disjoint_ball

added theorem Metric.closedBall_disjoint_closedBall

added theorem Metric.closedBall_eq_bInter_ball

added theorem Metric.closedBall_eq_empty

added theorem Metric.closedBall_mem_nhds

added theorem Metric.closedBall_mem_nhds_of_mem

added theorem Metric.closedBall_subset_ball'

added theorem Metric.closedBall_subset_ball

added theorem Metric.closedBall_subset_closedBall'

added theorem Metric.closedBall_subset_closedBall

added theorem Metric.closedBall_zero'

added theorem Metric.closedBall_zero

added theorem Metric.closedEmbedding_of_pairwise_le_dist

added theorem Metric.closure_ball_subset_closedBall

added theorem Metric.closure_closedBall

added theorem Metric.compactSpace_iff_bounded_univ

added theorem Metric.complete_of_cauchySeq_tendsto

added theorem Metric.complete_of_convergent_controlled_sequences

added theorem Metric.continuousAt_iff'

added theorem Metric.continuousAt_iff

added theorem Metric.continuousOn_iff'

added theorem Metric.continuousOn_iff

added theorem Metric.continuousWithinAt_iff'

added theorem Metric.continuousWithinAt_iff

added theorem Metric.continuous_iff'

added theorem Metric.continuous_iff

added theorem Metric.controlled_of_uniformEmbedding

added theorem Metric.denseRange_iff

added theorem Metric.dense_iff

added theorem Metric.diam_ball

added theorem Metric.diam_closedBall

added theorem Metric.diam_empty

added theorem Metric.diam_eq_zero_of_unbounded

added theorem Metric.diam_le_of_forall_dist_le

added theorem Metric.diam_le_of_forall_dist_le_of_nonempty

added theorem Metric.diam_le_of_subset_closedBall

added theorem Metric.diam_mono

added theorem Metric.diam_nonneg

added theorem Metric.diam_pair

added theorem Metric.diam_singleton

added theorem Metric.diam_subsingleton

added theorem Metric.diam_triple

added theorem Metric.diam_union'

added theorem Metric.diam_union

added theorem Metric.diam_univ_of_noncompact

added theorem Metric.dist_le_add_of_nonempty_closedBall_inter_closedBall

added theorem Metric.dist_le_diam_of_mem'

added theorem Metric.dist_le_diam_of_mem

added theorem Metric.dist_lt_add_of_nonempty_ball_inter_ball

added theorem Metric.dist_lt_add_of_nonempty_ball_inter_closedBall

added theorem Metric.dist_lt_add_of_nonempty_closedBall_inter_ball

added theorem Metric.dist_mem_uniformity

added theorem Metric.eball_top_eq_univ

added theorem Metric.ediam_le_of_forall_dist_le

added theorem Metric.ediam_of_unbounded

added theorem Metric.ediam_univ_eq_top_iff_noncompact

added theorem Metric.ediam_univ_of_noncompact

added theorem Metric.emetric_ball

added theorem Metric.emetric_ball_nnreal

added theorem Metric.emetric_ball_top

added theorem Metric.emetric_closedBall

added theorem Metric.emetric_closedBall_nnreal

added theorem Metric.eventually_nhds_iff

added theorem Metric.eventually_nhds_iff_ball

added theorem Metric.eventually_nhds_prod_iff

added theorem Metric.eventually_prod_nhds_iff

added theorem Metric.exists_ball_inter_eq_singleton_of_mem_discrete

added theorem Metric.exists_ball_subset_ball

added theorem Metric.exists_closedBall_inter_eq_singleton_of_discrete

added theorem Metric.exists_isOpen_bounded_image_inter_of_isCompact_of_continuousOn

added theorem Metric.exists_isOpen_bounded_image_inter_of_isCompact_of_forall_continuousWithinAt

added theorem Metric.exists_isOpen_bounded_image_of_isCompact_of_continuousOn

added theorem Metric.exists_isOpen_bounded_image_of_isCompact_of_forall_continuousAt

added theorem Metric.exists_local_min_mem_ball

added theorem Metric.exists_lt_mem_ball_of_mem_ball

added theorem Metric.finite_approx_of_totallyBounded

added theorem Metric.forall_of_forall_mem_ball

added theorem Metric.forall_of_forall_mem_closedBall

added theorem Metric.frontier_ball_subset_sphere

added theorem Metric.frontier_closedBall_subset_sphere

added theorem Metric.inseparable_iff

added theorem Metric.isBounded_iff

added theorem Metric.isBounded_iff_eventually

added theorem Metric.isBounded_iff_exists_ge

added theorem Metric.isBounded_iff_nndist

added theorem Metric.isClosed_ball

added theorem Metric.isClosed_of_pairwise_le_dist

added theorem Metric.isClosed_sphere

added theorem Metric.isCompact_iff_isClosed_bounded

added theorem Metric.isCompact_of_isClosed_bounded

added theorem Metric.isOpen_ball

added theorem Metric.isOpen_iff

added theorem Metric.isOpen_singleton_iff

added theorem Metric.mem_ball'

added theorem Metric.mem_ball

added theorem Metric.mem_ball_comm

added theorem Metric.mem_ball_self

added theorem Metric.mem_closedBall'

added theorem Metric.mem_closedBall

added theorem Metric.mem_closedBall_comm

added theorem Metric.mem_closedBall_self

added theorem Metric.mem_closure_iff

added theorem Metric.mem_closure_range_iff

added theorem Metric.mem_closure_range_iff_nat

added theorem Metric.mem_nhdsWithin_iff

added theorem Metric.mem_nhds_iff

added theorem Metric.mem_of_closed'

added theorem Metric.mem_sphere'

added theorem Metric.mem_sphere

added theorem Metric.mem_sphere_comm

added theorem Metric.mem_uniformity_dist

added theorem Metric.ne_of_mem_sphere

added theorem Metric.nhdsWithin_basis_ball

added theorem Metric.nhds_basis_ball

added theorem Metric.nhds_basis_ball_inv_nat_pos

added theorem Metric.nhds_basis_ball_inv_nat_succ

added theorem Metric.nhds_basis_ball_pow

added theorem Metric.nhds_basis_closedBall

added theorem Metric.nhds_basis_closedBall_pow

added theorem Metric.nonempty_ball

added theorem Metric.nonempty_closedBall

added theorem Metric.nonempty_interᵢ_of_nonempty_bInter

added theorem Metric.pos_of_mem_ball

added theorem Metric.secondCountable_of_almost_dense_set

added theorem Metric.secondCountable_of_countable_discretization

added def Metric.sphere

added theorem Metric.sphere_disjoint_ball

added theorem Metric.sphere_eq_empty_of_subsingleton

added theorem Metric.sphere_isEmpty_of_subsingleton

added theorem Metric.sphere_subset_closedBall

added theorem Metric.sphere_union_ball

added theorem Metric.sphere_zero

added theorem Metric.subsingleton_closedBall

added theorem Metric.subsingleton_sphere

added theorem Metric.tendstoLocallyUniformlyOn_iff

added theorem Metric.tendstoLocallyUniformly_iff

added theorem Metric.tendstoUniformlyOnFilter_iff

added theorem Metric.tendstoUniformlyOn_iff

added theorem Metric.tendstoUniformly_iff

added theorem Metric.tendsto_atTop

added theorem Metric.tendsto_at_top'

added theorem Metric.tendsto_nhds

added theorem Metric.tendsto_nhdsWithin_nhds

added theorem Metric.tendsto_nhdsWithin_nhdsWithin

added theorem Metric.tendsto_nhds_nhds

added theorem Metric.toUniformSpace_eq

added theorem Metric.totallyBounded_iff

added theorem Metric.totallyBounded_of_finite_discretization

added theorem Metric.uniformCauchySeqOn_iff

added theorem Metric.uniformContinuousOn_iff

added theorem Metric.uniformContinuousOn_iff_le

added theorem Metric.uniformContinuous_iff

added theorem Metric.uniformEmbedding_bot_of_pairwise_le_dist

added theorem Metric.uniformEmbedding_iff'

added theorem Metric.uniformity_basis_dist

added theorem Metric.uniformity_basis_dist_inv_nat_pos

added theorem Metric.uniformity_basis_dist_inv_nat_succ

added theorem Metric.uniformity_basis_dist_le

added theorem Metric.uniformity_basis_dist_le_pow

added theorem Metric.uniformity_basis_dist_lt

added theorem Metric.uniformity_basis_dist_pow

added theorem Metric.uniformity_basis_dist_rat

added theorem Metric.uniformity_edist

added theorem Metric.uniformity_edist_aux

added theorem Metric.uniformity_eq_comap_nhds_zero

added theorem Metric.unionᵢ_ball_nat

added theorem Metric.unionᵢ_ball_nat_succ

added theorem Metric.unionᵢ_closedBall_nat

added theorem Metric.unionᵢ_inter_closedBall_nat

added theorem MetricSpace.ext

added def MetricSpace.induced

added def MetricSpace.ofDistTopology

added def MetricSpace.ofT0PseudoMetricSpace

added def MetricSpace.replaceBornology

added theorem MetricSpace.replaceBornology_eq

added def MetricSpace.replaceTopology

added theorem MetricSpace.replaceTopology_eq

added def MetricSpace.replaceUniformity

added theorem MetricSpace.replaceUniformity_eq

added theorem MulOpposite.dist_op

added theorem MulOpposite.dist_unop

added theorem MulOpposite.nndist_op

added theorem MulOpposite.nndist_unop

added theorem NNReal.dist_eq

added theorem NNReal.le_add_nndist

added theorem NNReal.nndist_eq

added theorem NNReal.nndist_zero_eq_val'

added theorem NNReal.nndist_zero_eq_val

added theorem Prod.dist_eq

added def PseudoEMetricSpace.toPseudoMetricSpace

added def PseudoEMetricSpace.toPseudoMetricSpaceOfDist

added theorem PseudoMetricSpace.ext

added def PseudoMetricSpace.induced

added def PseudoMetricSpace.ofDistTopology

added def PseudoMetricSpace.replaceBornology

added theorem PseudoMetricSpace.replaceBornology_eq

added def PseudoMetricSpace.replaceTopology

added theorem PseudoMetricSpace.replaceTopology_eq

added def PseudoMetricSpace.replaceUniformity

added theorem PseudoMetricSpace.replaceUniformity_eq

added theorem Real.Icc_eq_closedBall

added theorem Real.Ioo_eq_ball

added theorem Real.ball_eq_Ioo

added theorem Real.closedBall_eq_Icc

added theorem Real.dist_0_eq_abs

added theorem Real.dist_eq

added theorem Real.dist_le_of_mem_Icc

added theorem Real.dist_le_of_mem_Icc_01

added theorem Real.dist_le_of_mem_pi_Icc

added theorem Real.dist_le_of_mem_uIcc

added theorem Real.dist_left_le_of_mem_uIcc

added theorem Real.dist_right_le_of_mem_uIcc

added theorem Real.nndist_eq'

added theorem Real.nndist_eq

added theorem Subtype.dist_eq

added theorem Subtype.nndist_eq

added theorem TotallyBounded.bounded

added theorem ULift.dist_eq

added theorem ULift.dist_up_up

added theorem ULift.nndist_eq

added theorem ULift.nndist_up_up

added def UniformEmbedding.comapMetricSpace

added def UniformInducing.comapPseudoMetricSpace

added theorem UniformSpace.SeparationQuotient.dist_mk

added def UniformSpace.ofDist

added theorem abs_dist

added theorem abs_dist_sub_le

added theorem ball_pi'

added theorem ball_pi

added theorem ball_prod_same

added theorem cauchySeq_bdd

added theorem cauchySeq_iff_le_tendsto_0

added theorem cauchySeq_iff_tendsto_dist_atTop_0

added theorem cauchySeq_of_le_tendsto_0'

added theorem cauchySeq_of_le_tendsto_0

added theorem closedBall_pi'

added theorem closedBall_pi

added theorem closedBall_prod_same

added theorem coe_nndist

added theorem coe_nnreal_ennreal_nndist

added theorem comap_dist_left_atTop_eq_cocompact

added theorem comap_dist_left_atTop_le_cocompact

added theorem comap_dist_right_atTop_eq_cocompact

added theorem comap_dist_right_atTop_le_cocompact

added theorem continuous_dist

added theorem continuous_iff_continuous_dist

added theorem continuous_nndist

added theorem dist_comm

added theorem dist_dist_dist_le

added theorem dist_dist_dist_le_left

added theorem dist_dist_dist_le_right

added theorem dist_edist

added theorem dist_eq_zero

added theorem dist_le_Ico_sum_dist

added theorem dist_le_Ico_sum_of_dist_le

added theorem dist_le_coe

added theorem dist_le_pi_dist

added theorem dist_le_range_sum_dist

added theorem dist_le_range_sum_of_dist_le

added theorem dist_le_zero

added theorem dist_lt_coe

added theorem dist_ne_zero

added theorem dist_nndist

added theorem dist_nonneg

added theorem dist_ofAdd

added theorem dist_ofDual

added theorem dist_ofMul

added theorem dist_pi_const

added theorem dist_pi_const_le

added theorem dist_pi_def

added theorem dist_pi_le_iff'

added theorem dist_pi_le_iff

added theorem dist_pi_lt_iff

added theorem dist_pos

added theorem dist_prod_same_left

added theorem dist_prod_same_right

added theorem dist_self

added theorem dist_toAdd

added theorem dist_toDual

added theorem dist_toMul

added theorem dist_triangle4

added theorem dist_triangle4_left

added theorem dist_triangle4_right

added theorem dist_triangle

added theorem dist_triangle_left

added theorem dist_triangle_right

added theorem edist_dist

added theorem edist_le_coe

added theorem edist_le_ofReal

added theorem edist_lt_coe

added theorem edist_lt_ofReal

added theorem edist_lt_top

added theorem edist_ne_top

added theorem edist_nndist

added theorem eq_of_dist_eq_zero

added theorem eq_of_forall_dist_le

added theorem eq_of_nndist_eq_zero

added theorem eventually_closedBall_subset

added theorem exists_lt_subset_ball

added theorem exists_pos_lt_subset_ball

added theorem finite_cover_balls_of_compact

added theorem isCompact_sphere

added theorem lebesgue_number_lemma_of_metric

added theorem lebesgue_number_lemma_of_metric_unionₛ

added theorem nhds_comap_dist

added theorem nndist_comm

added theorem nndist_dist

added theorem nndist_edist

added theorem nndist_eq_zero

added theorem nndist_le_pi_nndist

added theorem nndist_ofAdd

added theorem nndist_ofDual

added theorem nndist_ofMul

added theorem nndist_pi_const

added theorem nndist_pi_const_le

added theorem nndist_pi_def

added theorem nndist_pi_le_iff

added theorem nndist_self

added theorem nndist_toAdd

added theorem nndist_toDual

added theorem nndist_toMul

added theorem nndist_triangle

added theorem nndist_triangle_left

added theorem nndist_triangle_right

added theorem properSpace_of_compact_closedBall_of_le

added theorem squeeze_zero'

added theorem squeeze_zero

added theorem swap_dist

added theorem tendsto_cocompact_of_tendsto_dist_comp_atTop

added theorem tendsto_dist_left_cocompact_atTop

added theorem tendsto_dist_right_cocompact_atTop

added theorem tendsto_iff_dist_tendsto_zero

added theorem tendsto_iff_of_dist

added theorem tendsto_uniformity_iff_dist_tendsto_zero

added theorem totallyBounded_Icc

added theorem totallyBounded_Ico

added theorem totallyBounded_Ioc

added theorem totallyBounded_Ioo

added theorem uniformContinuous_dist

added theorem uniformContinuous_nndist

added theorem zero_eq_dist

added theorem zero_eq_nndist

Modified Mathlib/Topology/MetricSpace/EMetricSpace.lean

added theorem TopologicalSpace.IsSeparable.separableSpace