refactor(EMetricSpace): rename EMetric.ball -> Metric.eball

[urkud]

Also rename EMetric.closedBall -> Metric.closedEBall
and most (all?) of the related lemmas.

---

[github-actions]

PR summary e9d4384eb6

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ EMetric.measure_ball_pos
+ EMetric.measure_closedBall_pos
+ EMetric.t4Space
+ Metric.closedEBall_coe
+ Metric.closedEBall_ofReal
+ Metric.closedEBall_zero
+ Metric.eball_coe
+ Metric.eball_ofReal
+ Metric.eball_top
+ Metric.exists_contMDiffMap_forall_closedEBall_subset
+ Metric.isClosed_closedEBall
+ closedEBall
+ closedEBall_mem_nhds
+ closedEBall_prod_same
+ closedEBall_subset_closedEBall
+ closedEBall_top
+ eball
+ eball_disjoint
+ eball_eq_empty_iff
+ eball_mem_nhds
+ eball_prod_same
+ eball_subset
+ eball_subset_closedEBall
+ eball_subset_eball
+ eball_zero
+ edistLtTopSetoid
+ eventually_nhds_zero_forall_closedEBall_subset
+ exists_continuous_ennreal_forall_closedEBall_subset
+ exists_continuous_nnreal_forall_closedEBall_subset
+ exists_continuous_real_forall_closedEBall_subset
+ exists_eball_subset_eball
+ exists_forall_closedEBall_subset_aux₁
+ exists_forall_closedEBall_subset_aux₂
+ hasSum_taylorSeries_on_eball
+ image_ofSnowflaking_closedEBall
+ image_ofSnowflaking_eball
+ image_toSnowflaking_closedEBall
+ image_toSnowflaking_eball
+ isClosed_eball_top
+ isCover_iff_subset_iUnion_closedEBall
+ isOpen_eball
+ measure_closedEBall_pos
+ measure_eball_pos
+ mem_closedEBall
+ mem_closedEBall'
+ mem_closedEBall_comm
+ mem_closedEBall_self
+ mem_eball
+ mem_eball'
+ mem_eball_comm
+ mem_eball_one_iff
+ mem_eball_self
+ mem_emetric_ball_zero_iff
+ nhdsWithin_basis_closedEBall
+ nhds_basis_closedEBall
+ ordConnected_setOf_closedEBall_subset
+ ordConnected_setOf_eball_subset
+ pos_of_mem_eball
+ preimage_add_left_ball
+ preimage_add_left_closedBall
+ preimage_add_right_ball
+ preimage_add_right_closedBall
+ preimage_mul_left_closedEBall
+ preimage_mul_left_eball
+ preimage_mul_right_closedEBall
+ preimage_mul_right_eball
+ preimage_ofSnowflaking_closedEBall
+ preimage_ofSnowflaking_eball
+ preimage_smul_closedEBall
+ preimage_smul_eball
+ preimage_toSnowflaking_closedEBall
+ preimage_toSnowflaking_eball
+ preimage_vadd_ball
+ preimage_vadd_closedBall
+ smul_closedEBall
+ smul_eball
+ taylorSeries_eq_on_eball
+ taylorSeries_eq_on_eball'
+ vadd_ball
+ vadd_closedBall
+ volume_closedEBall
+ volume_eball
++ image_closedEBall
++ image_eball
+++ mapsTo_closedEBall
+++ mapsTo_eball
+++ preimage_closedEBall
+++ preimage_eball
+++--- mapsTo_emetric_ball
+++--- mapsTo_emetric_closedBall
++-- preimage_emetric_ball
++-- preimage_emetric_closedBall
+-+ nhdsWithin_basis_eball
+-+ nhds_basis_eball
- measure_ball_pos
- measure_closedBall_pos

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).