Commit 2024-08-16 01:08 f2871ace

View on Github →

chore: splitting up metric spaces files (#15790)

Estimated changes

deleted def EMetric.ball
deleted theorem EMetric.ball_disjoint
deleted theorem EMetric.ball_eq_empty_iff
deleted theorem EMetric.ball_mem_nhds
deleted theorem EMetric.ball_prod_same
deleted theorem EMetric.ball_subset
deleted theorem EMetric.ball_subset_ball
deleted theorem EMetric.ball_zero
deleted def EMetric.closedBall
deleted theorem EMetric.closedBall_top
deleted theorem EMetric.diam_ball
deleted theorem EMetric.diam_closedBall
deleted theorem EMetric.diam_empty
deleted theorem EMetric.diam_eq_sSup
deleted theorem EMetric.diam_eq_zero_iff
deleted theorem EMetric.diam_image_le_iff
deleted theorem EMetric.diam_insert
deleted theorem EMetric.diam_le
deleted theorem EMetric.diam_le_iff
deleted theorem EMetric.diam_mono
deleted theorem EMetric.diam_one
deleted theorem EMetric.diam_pair
deleted theorem EMetric.diam_pi_le_of_le
deleted theorem EMetric.diam_pos_iff'
deleted theorem EMetric.diam_pos_iff
deleted theorem EMetric.diam_singleton
deleted theorem EMetric.diam_subsingleton
deleted theorem EMetric.diam_triple
deleted theorem EMetric.diam_union'
deleted theorem EMetric.diam_union
deleted theorem EMetric.isClosed_ball_top
deleted theorem EMetric.isOpen_ball
deleted theorem EMetric.isOpen_iff
deleted theorem EMetric.mem_ball'
deleted theorem EMetric.mem_ball
deleted theorem EMetric.mem_ball_comm
deleted theorem EMetric.mem_ball_self
deleted theorem EMetric.mem_closedBall'
deleted theorem EMetric.mem_closedBall
deleted theorem EMetric.mem_closure_iff
deleted theorem EMetric.mem_nhds_iff
deleted theorem EMetric.nhds_basis_eball
deleted theorem EMetric.nhds_eq
deleted theorem EMetric.pos_of_mem_ball
deleted theorem EMetric.tendsto_atTop
deleted theorem EMetric.tendsto_nhds
deleted theorem EMetric.tendsto_nhds_nhds
deleted theorem MulOpposite.edist_op
deleted theorem MulOpposite.edist_unop
deleted theorem Prod.edist_eq
deleted theorem Subtype.edist_eq
deleted theorem ULift.edist_eq
deleted theorem ULift.edist_up_up
deleted theorem edist_congr
deleted theorem edist_congr_left
deleted theorem edist_congr_right
deleted theorem edist_eq_zero
deleted theorem edist_le_zero
deleted theorem edist_mem_uniformity
deleted theorem edist_ofAdd
deleted theorem edist_ofDual
deleted theorem edist_ofMul
deleted theorem edist_pos
deleted theorem edist_toAdd
deleted theorem edist_toDual
deleted theorem edist_toMul
deleted theorem edist_triangle4
deleted theorem edist_triangle_left
deleted theorem edist_triangle_right
deleted theorem eq_of_forall_edist_le
deleted theorem mem_uniformity_edist
deleted def uniformSpaceOfEDist
deleted theorem uniformSpace_edist
deleted theorem uniformity_basis_edist'
deleted theorem uniformity_basis_edist
deleted theorem uniformity_basis_edist_le
deleted theorem uniformity_edist
deleted theorem uniformity_pseudoedist
deleted theorem zero_eq_edist
added def EMetric.ball
added theorem EMetric.ball_disjoint
added theorem EMetric.ball_mem_nhds
added theorem EMetric.ball_prod_same
added theorem EMetric.ball_subset
added theorem EMetric.ball_zero
added theorem EMetric.closedBall_top
added theorem EMetric.isOpen_ball
added theorem EMetric.isOpen_iff
added theorem EMetric.mem_ball'
added theorem EMetric.mem_ball
added theorem EMetric.mem_ball_comm
added theorem EMetric.mem_ball_self
added theorem EMetric.mem_closedBall
added theorem EMetric.mem_nhds_iff
added theorem EMetric.nhds_eq
added theorem EMetric.tendsto_atTop
added theorem EMetric.tendsto_nhds
added theorem MulOpposite.edist_op
added theorem MulOpposite.edist_unop
added theorem Prod.edist_eq
added theorem Subtype.edist_eq
added theorem ULift.edist_eq
added theorem ULift.edist_up_up
added theorem edist_congr
added theorem edist_congr_left
added theorem edist_congr_right
added theorem edist_eq_zero
added theorem edist_le_zero
added theorem edist_mem_uniformity
added theorem edist_ofAdd
added theorem edist_ofDual
added theorem edist_ofMul
added theorem edist_pos
added theorem edist_toAdd
added theorem edist_toDual
added theorem edist_toMul
added theorem edist_triangle4
added theorem edist_triangle_left
added theorem edist_triangle_right
added theorem eq_of_forall_edist_le
added theorem mem_uniformity_edist
added theorem uniformSpace_edist
added theorem uniformity_basis_edist
added theorem uniformity_edist
added theorem uniformity_pseudoedist
added theorem zero_eq_edist
added theorem EMetric.diam_ball
added theorem EMetric.diam_empty
added theorem EMetric.diam_eq_sSup
added theorem EMetric.diam_insert
added theorem EMetric.diam_le
added theorem EMetric.diam_le_iff
added theorem EMetric.diam_mono
added theorem EMetric.diam_one
added theorem EMetric.diam_pair
added theorem EMetric.diam_pos_iff'
added theorem EMetric.diam_pos_iff
added theorem EMetric.diam_singleton
added theorem EMetric.diam_triple
added theorem EMetric.diam_union'
added theorem EMetric.diam_union
deleted theorem Metric.closedBall_zero
deleted theorem Metric.sphere_zero
deleted theorem MetricSpace.ext
deleted theorem dist_eq_zero
deleted theorem dist_le_zero
deleted theorem dist_ne_zero
deleted theorem dist_ofAdd
deleted theorem dist_ofDual
deleted theorem dist_ofMul
deleted theorem dist_pos
deleted theorem dist_toAdd
deleted theorem dist_toDual
deleted theorem dist_toMul
deleted theorem eq_of_dist_eq_zero
deleted theorem eq_of_forall_dist_le
deleted theorem eq_of_nndist_eq_zero
deleted theorem nndist_eq_zero
deleted theorem nndist_ofAdd
deleted theorem nndist_ofDual
deleted theorem nndist_ofMul
deleted theorem nndist_toAdd
deleted theorem nndist_toDual
deleted theorem nndist_toMul
deleted theorem zero_eq_dist
deleted theorem zero_eq_nndist
added theorem Metric.closedBall_zero
added theorem Metric.sphere_zero
added theorem MetricSpace.ext
added theorem dist_eq_zero
added theorem dist_le_zero
added theorem dist_ne_zero
added theorem dist_ofAdd
added theorem dist_ofDual
added theorem dist_ofMul
added theorem dist_pos
added theorem dist_toAdd
added theorem dist_toDual
added theorem dist_toMul
added theorem eq_of_dist_eq_zero
added theorem eq_of_forall_dist_le
added theorem eq_of_nndist_eq_zero
added theorem nndist_eq_zero
added theorem nndist_ofAdd
added theorem nndist_ofDual
added theorem nndist_ofMul
added theorem nndist_toAdd
added theorem nndist_toDual
added theorem nndist_toMul
added theorem zero_eq_dist
added theorem zero_eq_nndist
added theorem IsCompact.isSeparable
added theorem Metric.inseparable_iff
added theorem dist_le_Ico_sum_dist
added theorem dist_le_range_sum_dist
deleted theorem ball_pi'
deleted theorem ball_pi
deleted theorem closedBall_pi'
deleted theorem closedBall_pi
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 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 IsCompact.isSeparable
deleted theorem Metric.inseparable_iff
deleted theorem Metric.totallyBounded_iff
deleted theorem dist_le_Ico_sum_dist
deleted theorem dist_le_range_sum_dist
deleted theorem Real.dist_le_of_mem_Icc
deleted theorem Real.dist_le_of_mem_uIcc
added theorem ball_pi'
added theorem ball_pi
added theorem closedBall_pi'
added theorem closedBall_pi
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 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