Commit 2023-10-30 10:24 2904132a

View on Github →

chore: split MetricSpace.basic (#7920) This reduces the main file from 3340 to 2220 lines. The remaining file is somewhat entangled, so splitting is less obvious. Help is welcome, though a follow-up PR is probably better :-) I've kept copyright and authors as they were originally.

Estimated changes

deleted def Bornology.ofDist
deleted theorem CauchySeq.isBounded_range
deleted theorem Dense.exists_dist_lt
deleted theorem Filter.Tendsto.congr_dist
deleted theorem IsCompact.isBounded
deleted theorem IsCompact.isSeparable
deleted def Metric.ball
deleted theorem Metric.ball_disjoint_ball
deleted theorem Metric.ball_eq_ball'
deleted theorem Metric.ball_eq_ball
deleted theorem Metric.ball_eq_empty
deleted theorem Metric.ball_half_subset
deleted theorem Metric.ball_mem_nhds
deleted theorem Metric.ball_subset
deleted theorem Metric.ball_subset_ball'
deleted theorem Metric.ball_subset_ball
deleted theorem Metric.ball_union_sphere
deleted theorem Metric.ball_zero
deleted theorem Metric.cauchySeq_iff'
deleted theorem Metric.cauchySeq_iff
deleted def Metric.closedBall
deleted theorem Metric.closedBall_zero'
deleted theorem Metric.closure_closedBall
deleted theorem Metric.closure_sphere
deleted theorem Metric.continuousAt_iff'
deleted theorem Metric.continuousAt_iff
deleted theorem Metric.continuousOn_iff'
deleted theorem Metric.continuousOn_iff
deleted theorem Metric.continuous_iff'
deleted theorem Metric.continuous_iff
deleted theorem Metric.denseRange_iff
deleted theorem Metric.dense_iff
deleted theorem Metric.diam_ball
deleted theorem Metric.diam_closedBall
deleted theorem Metric.diam_empty
deleted theorem Metric.diam_mono
deleted theorem Metric.diam_nonneg
deleted theorem Metric.diam_pair
deleted theorem Metric.diam_singleton
deleted theorem Metric.diam_subsingleton
deleted theorem Metric.diam_triple
deleted theorem Metric.diam_union'
deleted theorem Metric.diam_union
deleted theorem Metric.eball_top_eq_univ
deleted theorem Metric.ediam_of_unbounded
deleted theorem Metric.emetric_ball
deleted theorem Metric.emetric_ball_top
deleted theorem Metric.emetric_closedBall
deleted theorem Metric.iUnion_ball_nat
deleted theorem Metric.inseparable_iff
deleted theorem Metric.isBounded_Icc
deleted theorem Metric.isBounded_Ico
deleted theorem Metric.isBounded_Ioc
deleted theorem Metric.isBounded_Ioo
deleted theorem Metric.isBounded_ball
deleted theorem Metric.isBounded_iff
deleted theorem Metric.isBounded_sphere
deleted theorem Metric.isClosed_ball
deleted theorem Metric.isClosed_sphere
deleted theorem Metric.isOpen_ball
deleted theorem Metric.isOpen_iff
deleted theorem Metric.mem_ball'
deleted theorem Metric.mem_ball
deleted theorem Metric.mem_ball_comm
deleted theorem Metric.mem_ball_self
deleted theorem Metric.mem_closedBall'
deleted theorem Metric.mem_closedBall
deleted theorem Metric.mem_closure_iff
deleted theorem Metric.mem_nhdsWithin_iff
deleted theorem Metric.mem_nhds_iff
deleted theorem Metric.mem_of_closed'
deleted theorem Metric.mem_sphere'
deleted theorem Metric.mem_sphere
deleted theorem Metric.mem_sphere_comm
deleted theorem Metric.ne_of_mem_sphere
deleted theorem Metric.nhds_basis_ball
deleted theorem Metric.nonempty_ball
deleted theorem Metric.pos_of_mem_ball
deleted def Metric.sphere
deleted theorem Metric.sphere_subset_ball
deleted theorem Metric.sphere_union_ball
deleted theorem Metric.tendsto_atTop'
deleted theorem Metric.tendsto_atTop
deleted theorem Metric.tendsto_nhds
deleted theorem Metric.tendsto_nhds_nhds
deleted theorem Metric.toUniformSpace_eq
deleted theorem Metric.totallyBounded_iff
deleted theorem Metric.uniformity_edist
deleted theorem MulOpposite.dist_op
deleted theorem MulOpposite.dist_unop
deleted theorem MulOpposite.nndist_op
deleted theorem MulOpposite.nndist_unop
deleted theorem NNReal.dist_eq
deleted theorem NNReal.le_add_nndist
deleted theorem NNReal.nndist_eq
deleted theorem NNReal.nndist_zero_eq_val
deleted theorem Prod.dist_eq
deleted theorem PseudoMetricSpace.ext
deleted theorem Real.Icc_eq_closedBall
deleted theorem Real.Ioo_eq_ball
deleted theorem Real.ball_eq_Ioo
deleted theorem Real.closedBall_eq_Icc
deleted theorem Real.dist_0_eq_abs
deleted theorem Real.dist_eq
deleted theorem Real.dist_le_of_mem_Icc
deleted theorem Real.dist_le_of_mem_uIcc
deleted theorem Real.nndist_eq'
deleted theorem Real.nndist_eq
deleted theorem Subtype.dist_eq
deleted theorem Subtype.nndist_eq
deleted theorem TotallyBounded.isBounded
deleted theorem ULift.dist_eq
deleted theorem ULift.dist_up_up
deleted theorem ULift.nndist_eq
deleted theorem ULift.nndist_up_up
deleted def UniformSpace.ofDist
deleted theorem abs_dist
deleted theorem abs_dist_sub_le
deleted theorem ball_pi'
deleted theorem ball_pi
deleted theorem ball_prod_same
deleted theorem cauchySeq_bdd
deleted theorem cauchySeq_of_le_tendsto_0
deleted theorem closedBall_pi'
deleted theorem closedBall_pi
deleted theorem closedBall_prod_same
deleted theorem coe_nndist
deleted theorem coe_nnreal_ennreal_nndist
deleted theorem continuous_dist
deleted theorem continuous_nndist
deleted theorem dist_comm
deleted theorem dist_dist_dist_le
deleted theorem dist_dist_dist_le_left
deleted theorem dist_dist_dist_le_right
deleted theorem dist_edist
deleted theorem dist_le_Ico_sum_dist
deleted theorem dist_le_coe
deleted theorem dist_le_pi_dist
deleted theorem dist_le_range_sum_dist
deleted theorem dist_lt_coe
deleted theorem dist_nndist
deleted theorem dist_nonneg
deleted theorem dist_pi_const
deleted theorem dist_pi_const_le
deleted theorem dist_pi_def
deleted theorem dist_pi_eq_iff
deleted theorem dist_pi_le_iff'
deleted theorem dist_pi_le_iff
deleted theorem dist_pi_lt_iff
deleted theorem dist_prod_same_left
deleted theorem dist_prod_same_right
deleted theorem dist_self
deleted theorem dist_triangle4
deleted theorem dist_triangle4_left
deleted theorem dist_triangle4_right
deleted theorem dist_triangle
deleted theorem dist_triangle_left
deleted theorem dist_triangle_right
deleted theorem edist_dist
deleted theorem edist_le_coe
deleted theorem edist_le_ofReal
deleted theorem edist_lt_coe
deleted theorem edist_lt_ofReal
deleted theorem edist_lt_top
deleted theorem edist_ne_top
deleted theorem edist_nndist
deleted theorem exists_lt_subset_ball
deleted theorem exists_pos_lt_subset_ball
deleted theorem isCompact_sphere
deleted theorem nhds_comap_dist
deleted theorem nndist_comm
deleted theorem nndist_dist
deleted theorem nndist_edist
deleted theorem nndist_le_pi_nndist
deleted theorem nndist_pi_const
deleted theorem nndist_pi_const_le
deleted theorem nndist_pi_def
deleted theorem nndist_pi_eq_iff
deleted theorem nndist_pi_le_iff
deleted theorem nndist_pi_lt_iff
deleted theorem nndist_self
deleted theorem nndist_triangle
deleted theorem nndist_triangle_left
deleted theorem nndist_triangle_right
deleted theorem sphere_pi
deleted theorem sphere_prod
deleted theorem squeeze_zero'
deleted theorem squeeze_zero
deleted theorem swap_dist
deleted theorem tendsto_iff_of_dist
deleted theorem totallyBounded_Icc
deleted theorem totallyBounded_Ico
deleted theorem totallyBounded_Ioc
deleted theorem totallyBounded_Ioo
deleted theorem uniformContinuous_dist
deleted theorem uniformContinuous_nndist
added theorem IsCompact.isBounded
added theorem Metric.diam_ball
added theorem Metric.diam_closedBall
added theorem Metric.diam_empty
added theorem Metric.diam_mono
added theorem Metric.diam_nonneg
added theorem Metric.diam_pair
added theorem Metric.diam_singleton
added theorem Metric.diam_triple
added theorem Metric.diam_union'
added theorem Metric.diam_union
added theorem Metric.isBounded_Icc
added theorem Metric.isBounded_Ico
added theorem Metric.isBounded_Ioc
added theorem Metric.isBounded_Ioo
added theorem Metric.isBounded_ball
added theorem Metric.cauchySeq_iff'
added theorem Metric.cauchySeq_iff
added theorem cauchySeq_bdd
added def Bornology.ofDist
added theorem Dense.exists_dist_lt
added theorem IsCompact.isSeparable
added def Metric.ball
added theorem Metric.ball_eq_ball'
added theorem Metric.ball_eq_ball
added theorem Metric.ball_eq_empty
added theorem Metric.ball_mem_nhds
added theorem Metric.ball_subset
added theorem Metric.ball_zero
added theorem Metric.closure_sphere
added theorem Metric.continuous_iff'
added theorem Metric.continuous_iff
added theorem Metric.denseRange_iff
added theorem Metric.dense_iff
added theorem Metric.emetric_ball
added theorem Metric.iUnion_ball_nat
added theorem Metric.inseparable_iff
added theorem Metric.isBounded_iff
added theorem Metric.isClosed_ball
added theorem Metric.isClosed_sphere
added theorem Metric.isOpen_ball
added theorem Metric.isOpen_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_closure_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.nhds_basis_ball
added theorem Metric.nonempty_ball
added theorem Metric.pos_of_mem_ball
added def Metric.sphere
added theorem Metric.tendsto_atTop'
added theorem Metric.tendsto_atTop
added theorem Metric.tendsto_nhds
added theorem MulOpposite.dist_op
added theorem MulOpposite.dist_unop
added theorem MulOpposite.nndist_op
added theorem NNReal.dist_eq
added theorem NNReal.le_add_nndist
added theorem NNReal.nndist_eq
added theorem Prod.dist_eq
added theorem PseudoMetricSpace.ext
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.nndist_eq'
added theorem Real.nndist_eq
added theorem Subtype.dist_eq
added theorem Subtype.nndist_eq
added theorem ULift.dist_eq
added theorem ULift.dist_up_up
added theorem ULift.nndist_eq
added theorem ULift.nndist_up_up
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 closedBall_pi'
added theorem closedBall_pi
added theorem closedBall_prod_same
added theorem coe_nndist
added theorem 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_edist
added theorem dist_le_Ico_sum_dist
added theorem dist_le_coe
added theorem dist_le_pi_dist
added theorem dist_le_range_sum_dist
added theorem dist_lt_coe
added theorem dist_nndist
added theorem dist_nonneg
added theorem dist_pi_const
added theorem dist_pi_const_le
added theorem dist_pi_def
added theorem dist_pi_eq_iff
added theorem dist_pi_le_iff'
added theorem dist_pi_le_iff
added theorem dist_pi_lt_iff
added theorem dist_prod_same_left
added theorem dist_prod_same_right
added theorem dist_self
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 exists_lt_subset_ball
added theorem isCompact_sphere
added theorem nhds_comap_dist
added theorem nndist_comm
added theorem nndist_dist
added theorem nndist_edist
added theorem nndist_le_pi_nndist
added theorem nndist_pi_const
added theorem nndist_pi_const_le
added theorem nndist_pi_def
added theorem nndist_pi_eq_iff
added theorem nndist_pi_le_iff
added theorem nndist_pi_lt_iff
added theorem nndist_self
added theorem nndist_triangle
added theorem nndist_triangle_left
added theorem nndist_triangle_right
added theorem sphere_pi
added theorem sphere_prod
added theorem squeeze_zero'
added theorem squeeze_zero
added theorem swap_dist
added theorem tendsto_iff_of_dist
added theorem totallyBounded_Icc
added theorem totallyBounded_Ico
added theorem totallyBounded_Ioc
added theorem totallyBounded_Ioo
added theorem uniformContinuous_dist