Commit 2026-02-01 00:20 c4e24355

View on Github →

refactor(EMetricSpace): rename EMetric.ball -> Metric.eball (#34379) Also rename EMetric.closedBall -> Metric.closedEBall and most (all?) of the related lemmas.

Estimated changes

added theorem mem_eball_one_iff
deleted theorem mem_emetric_ball_one_iff
modified theorem measurableSet_eball
added theorem Real.volume_eball
deleted theorem Real.volume_emetric_ball
deleted theorem EMetric.measure_ball_pos
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.closedBall_zero
modified theorem EMetric.dense_iff
deleted theorem EMetric.isClosed_ball_top
deleted theorem EMetric.isOpen_ball
modified 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
modified theorem EMetric.mem_nhdsWithin_iff
modified theorem EMetric.mem_nhds_iff
deleted theorem EMetric.nhds_basis_eball
modified theorem EMetric.nhds_eq
deleted theorem EMetric.pos_of_mem_ball
added theorem Metric.closedEBall_top
added def Metric.eball
added theorem Metric.eball_disjoint
added theorem Metric.eball_mem_nhds
added theorem Metric.eball_prod_same
added theorem Metric.eball_subset
added theorem Metric.eball_zero
added theorem Metric.isOpen_eball
added theorem Metric.mem_closedEBall
added theorem Metric.mem_eball'
added theorem Metric.mem_eball
added theorem Metric.mem_eball_comm
added theorem Metric.mem_eball_self
added theorem Subtype.image_eball
deleted theorem Subtype.image_emetricBall
added theorem Subtype.preimage_eball
modified theorem Metric.ediam_closedEBall_le
modified theorem Metric.ediam_eball_le
deleted theorem EMetric.t4Space
added theorem Metric.t4Space
modified theorem edist_ne_top_of_mem_ball
modified theorem nhds_eq_nhds_emetric_ball
added theorem Dilation.mapsTo_eball
deleted theorem EMetric.smul_ball
deleted theorem EMetric.smul_closedBall
added theorem Metric.smul_eball
added theorem Isometry.mapsTo_eball
added theorem Metric.closedEBall_coe
added theorem Metric.eball_coe
added theorem Metric.eball_ofReal
added theorem Metric.eball_top
modified theorem Metric.eball_top_eq_univ
deleted theorem Metric.emetric_ball
deleted theorem Metric.emetric_ball_top
deleted theorem Metric.emetric_closedBall