Commit 2024-06-23 22:42 fca6b3ac

View on Github →

chore(Topology/MetricSpace/PseudoMetric): Split (#13977) This reduces the long pole.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/BoxIntegral/Box/Basic.lean

Modified Mathlib/Analysis/Convex/Extrema.lean

Modified Mathlib/Analysis/Normed/Group/Basic.lean

Modified Mathlib/Topology/Instances/Int.lean

Modified Mathlib/Topology/MetricSpace/Basic.lean

Modified Mathlib/Topology/MetricSpace/Cauchy.lean

Modified Mathlib/Topology/MetricSpace/Equicontinuity.lean

Modified Mathlib/Topology/MetricSpace/ProperSpace.lean

Created Mathlib/Topology/MetricSpace/Pseudo/Constructions.lean

added theorem Fin.dist_insertNth_insertNth

added theorem Fin.nndist_insertNth_insertNth

added def Inducing.comapPseudoMetricSpace

added theorem MulOpposite.dist_op

added theorem MulOpposite.dist_unop

added theorem MulOpposite.nndist_op

added theorem MulOpposite.nndist_unop

added theorem NNReal.ball_zero_eq_Ico'

added theorem NNReal.ball_zero_eq_Ico

added theorem NNReal.closedBall_zero_eq_Icc'

added theorem NNReal.closedBall_zero_eq_Icc

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 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 def UniformInducing.comapPseudoMetricSpace

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 continuous_dist

added theorem continuous_iff_continuous_dist

added theorem continuous_nndist

added theorem dist_le_pi_dist

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 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 sphere_pi

added theorem sphere_prod

added theorem uniformContinuous_dist

added theorem uniformContinuous_nndist

Renamed Mathlib/Topology/MetricSpace/PseudoMetric.lean to Mathlib/Topology/MetricSpace/Pseudo/Defs.lean

deleted theorem Fin.dist_insertNth_insertNth

deleted theorem Fin.nndist_insertNth_insertNth

deleted def Inducing.comapPseudoMetricSpace

deleted theorem Metric.closedBall_zero'

deleted theorem Metric.closure_ball_subset_closedBall

deleted theorem Metric.closure_closedBall

deleted theorem Metric.closure_sphere

deleted theorem Metric.eventually_isCompact_closedBall

deleted theorem Metric.exists_isCompact_closedBall

deleted theorem Metric.frontier_ball_subset_sphere

deleted theorem Metric.frontier_closedBall_subset_sphere

deleted theorem Metric.isClosed_ball

deleted theorem Metric.isClosed_sphere

deleted theorem MulOpposite.dist_op

deleted theorem MulOpposite.dist_unop

deleted theorem MulOpposite.nndist_op

deleted theorem MulOpposite.nndist_unop

deleted theorem NNReal.ball_zero_eq_Ico'

deleted theorem NNReal.ball_zero_eq_Ico

deleted theorem NNReal.closedBall_zero_eq_Icc'

deleted theorem NNReal.closedBall_zero_eq_Icc

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 NNReal.nndist_zero_eq_val

deleted theorem Prod.dist_eq

deleted theorem Real.dist_le_of_mem_Icc

deleted theorem Real.dist_le_of_mem_Icc_01

deleted theorem Real.dist_le_of_mem_pi_Icc

deleted theorem Real.dist_le_of_mem_uIcc

deleted theorem Real.dist_left_le_of_mem_uIcc

deleted theorem Real.dist_right_le_of_mem_uIcc

deleted theorem Subtype.dist_eq

deleted theorem Subtype.nndist_eq

deleted theorem ULift.dist_eq

deleted theorem ULift.dist_up_up

deleted theorem ULift.nndist_eq

deleted theorem ULift.nndist_up_up

deleted def UniformInducing.comapPseudoMetricSpace

deleted theorem ball_pi'

deleted theorem ball_pi

deleted theorem ball_prod_same

deleted theorem closedBall_pi'

deleted theorem closedBall_pi

deleted theorem closedBall_prod_same

deleted theorem continuous_dist

deleted theorem continuous_iff_continuous_dist

deleted theorem continuous_nndist

deleted theorem dist_le_pi_dist

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 eventually_closedBall_subset

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 sphere_pi

deleted theorem sphere_prod

deleted theorem squeeze_zero'

deleted theorem squeeze_zero

deleted theorem tendsto_closedBall_smallSets

deleted theorem uniformContinuous_dist

deleted theorem uniformContinuous_nndist

Created Mathlib/Topology/MetricSpace/Pseudo/Lemmas.lean

added theorem Metric.closedBall_zero'

added theorem Metric.closure_ball_subset_closedBall

added theorem Metric.closure_closedBall

added theorem Metric.closure_sphere

added theorem Metric.eventually_isCompact_closedBall

added theorem Metric.exists_isCompact_closedBall

added theorem Metric.frontier_ball_subset_sphere

added theorem Metric.frontier_closedBall_subset_sphere

added theorem Metric.isClosed_ball

added theorem Metric.isClosed_sphere

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 eventually_closedBall_subset

added theorem squeeze_zero'

added theorem squeeze_zero

added theorem tendsto_closedBall_smallSets

Modified scripts/style-exceptions.txt