Commit 2026-01-12 10:53 23a3f86b

chore(*): rename EMetric.infEdist -> Metric.infEDist etc (#33772) Moves:

• ConvexBody.hausdorffEdist_coe -> ConvexBody.hausdorffEDist_coe
• ConvexBody.hausdorffEdist_ne_top -> ConvexBody.hausdorffEDist_ne_top
• EMetric.Closeds.edist_eq -> TopologicalSpace.Closeds.edist_eq
• EMetric.Closeds.isometry_singleton -> TopologicalSpace.Closeds.isometry_singleton
• EMetric.Closeds.lipschitz_sup -> TopologicalSpace.Closeds.lipschitz_sup
• EMetric.NonemptyCompacts.isClosed_in_closeds -> TopologicalSpace.NonemptyCompacts.isClosed_in_closeds
• EMetric.NonemptyCompacts.isometry_singleton -> TopologicalSpace.NonemptyCompacts.isometry_singleton
• EMetric.NonemptyCompacts.isometry_toCloseds -> TopologicalSpace.NonemptyCompacts.isometry_toCloseds
• EMetric.NonemptyCompacts.lipschitz_prod -> TopologicalSpace.NonemptyCompacts.lipschitz_prod
• EMetric.NonemptyCompacts.lipschitz_sup -> TopologicalSpace.NonemptyCompacts.lipschitz_sup
• EMetric.continuous_infEdist -> Metric.continuous_infEDist
• EMetric.continuous_infEdist_hausdorffEdist -> TopologicalSpace.Closeds.continuous_infEDist
• EMetric.disjoint_closedBall_of_lt_infEdist -> Metric.disjoint_closedEBall_of_lt_infEDist
• EMetric.edist_le_infEdist_add_ediam -> Metric.edist_le_infEDist_add_ediam
• EMetric.empty_or_nonempty_of_hausdorffEdist_ne_top -> Metric.empty_or_nonempty_of_hausdorffEDist_ne_top
• EMetric.exists_edist_lt_of_hausdorffEdist_lt -> Metric.exists_edist_lt_of_hausdorffEDist_lt
• EMetric.exists_pos_forall_lt_edist -> Metric.exists_pos_forall_lt_edist
• EMetric.exists_real_pos_lt_infEdist_of_notMem_closure -> Metric.exists_real_pos_lt_infEDist_of_notMem_closure
• EMetric.hausdorffEdist -> Metric.hausdorffEDist
• EMetric.hausdorffEdist_closure -> Metric.hausdorffEDist_closure
• EMetric.hausdorffEdist_closure₁ -> Metric.hausdorffEDist_closure_left
• EMetric.hausdorffEdist_closure₂ -> Metric.hausdorffEDist_closure_right
• EMetric.hausdorffEdist_comm -> Metric.hausdorffEDist_comm
• EMetric.hausdorffEdist_def -> Metric.hausdorffEDist_def
• EMetric.hausdorffEdist_empty -> Metric.hausdorffEDist_empty
• EMetric.hausdorffEdist_iUnion_le -> Metric.hausdorffEDist_iUnion_le
• EMetric.hausdorffEdist_image -> Metric.hausdorffEDist_image
• EMetric.hausdorffEdist_le_ediam -> Metric.hausdorffEDist_le_ediam
• EMetric.hausdorffEdist_le_of_infEdist -> Metric.hausdorffEDist_le_of_infEDist
• EMetric.hausdorffEdist_le_of_mem_edist -> Metric.hausdorffEDist_le_of_mem_edist
• EMetric.hausdorffEdist_le_of_mem_hausdorffEntourage -> Metric.hausdorffEDist_le_of_mem_hausdorffEntourage
• EMetric.hausdorffEdist_prod_le -> Metric.hausdorffEDist_prod_le
• EMetric.hausdorffEdist_self -> Metric.hausdorffEDist_self
• EMetric.hausdorffEdist_self_closure -> Metric.hausdorffEDist_self_closure
• EMetric.hausdorffEdist_singleton -> Metric.hausdorffEDist_singleton
• EMetric.hausdorffEdist_triangle -> Metric.hausdorffEDist_triangle
• EMetric.hausdorffEdist_union_le -> Metric.hausdorffEDist_union_le
• EMetric.hausdorffEdist_zero_iff_closure_eq_closure -> Metric.hausdorffEDist_zero_iff_closure_eq_closure
• EMetric.hausdorffEdist_zero_iff_eq_of_closed -> IsClosed.hausdorffEDist_zero_iff
• EMetric.infEdist -> Metric.infEDist
• EMetric.infEdist_anti -> Metric.infEDist_anti
• EMetric.infEdist_biUnion -> Metric.infEDist_biUnion
• EMetric.infEdist_closure -> Metric.infEDist_closure
• EMetric.infEdist_closure_pos_iff_notMem_closure -> Metric.infEDist_closure_pos_iff_notMem_closure
• EMetric.infEdist_empty -> Metric.infEDist_empty
• EMetric.infEdist_iUnion -> Metric.infEDist_iUnion
• EMetric.infEdist_image -> Metric.infEDist_image
• EMetric.infEdist_le_edist_add_infEdist -> Metric.infEDist_le_edist_add_infEDist
• EMetric.infEdist_le_edist_of_mem -> Metric.infEDist_le_edist_of_mem
• EMetric.infEdist_le_hausdorffEdist_of_mem -> Metric.infEDist_le_hausdorffEDist_of_mem
• EMetric.infEdist_le_infEdist_add_edist -> Metric.infEDist_le_infEDist_add_edist
• EMetric.infEdist_le_infEdist_add_hausdorffEdist -> Metric.infEDist_le_infEDist_add_hausdorffEDist
• EMetric.infEdist_lt_iff -> Metric.infEDist_lt_iff
• EMetric.infEdist_pos_iff_notMem_closure -> Metric.infEDist_pos_iff_notMem_closure
• EMetric.infEdist_prod -> Metric.infEDist_prod
• EMetric.infEdist_singleton -> Metric.infEDist_singleton
• EMetric.infEdist_smul -> Metric.infEDist_smul
• EMetric.infEdist_union -> Metric.infEDist_union
• EMetric.infEdist_vadd -> Metric.infEDist_vadd
• EMetric.infEdist_zero_of_mem -> Metric.infEDist_zero_of_mem
• EMetric.le_infEdist -> Metric.le_infEDist
• EMetric.mem_closure_iff_infEdist_zero -> Metric.mem_closure_iff_infEDist_zero
• EMetric.mem_hausdorffEntourage_of_hausdorffEdist_lt -> Metric.mem_hausdorffEntourage_of_hausdorffEDist_lt
• EMetric.mem_iff_infEdist_zero_of_closed -> Metric.mem_iff_infEDist_zero_of_closed
• EMetric.nonempty_of_hausdorffEdist_ne_top -> Metric.nonempty_of_hausdorffEDist_ne_top
• EmetricSpace.ofRiemannianMetric -> EMetricSpace.ofRiemannianMetric
• IsCompact.exists_infEdist_eq_edist -> IsCompact.exists_infEDist_eq_edist
• Measurable.infEdist -> Measurable.infEDist
• Metric.cthickening_eq_preimage_infEdist -> Metric.cthickening_eq_preimage_infEDist
• Metric.eventually_notMem_cthickening_of_infEdist_pos -> Metric.eventually_notMem_cthickening_of_infEDist_pos
• Metric.eventually_notMem_thickening_of_infEdist_pos -> Metric.eventually_notMem_thickening_of_infEDist_pos
• Metric.hausdorffEdist_ne_top_of_nonempty_of_bounded -> Metric.hausdorffEDist_ne_top_of_nonempty_of_bounded
• Metric.infEdist_eq_top_iff -> Metric.infEDist_eq_top_iff
• Metric.infEdist_le_infEdist_cthickening_add -> Metric.infEDist_le_infEDist_cthickening_add
• Metric.infEdist_le_infEdist_thickening_add -> Metric.infEDist_le_infEDist_thickening_add
• Metric.infEdist_ne_top -> Metric.infEDist_ne_top
• Metric.mem_thickening_iff_infEdist_lt -> Metric.mem_thickening_iff_infEDist_lt
• Metric.thickening_eq_preimage_infEdist -> Metric.thickening_eq_preimage_infEDist
• PseudoEmetricSpace.ofEdistOfTopology -> PseudoEMetricSpace.ofEDistOfTopology
• PseudoEmetricSpace.ofRiemannianMetric -> PseudoEMetricSpace.ofRiemannianMetric
• infEdist_cthickening -> infEDist_cthickening
• infEdist_inv -> infEDist_inv
• infEdist_inv_inv -> infEDist_inv_inv
• infEdist_neg -> infEDist_neg
• infEdist_neg_neg -> infEDist_neg_neg
• infEdist_smul₀ -> infEDist_smul₀
• infEdist_thickening -> infEDist_thickening
• measurable_infEdist -> measurable_infEDist
• thickenedIndicatorAux_mono_infEdist -> thickenedIndicatorAux_mono_infEDist
• thickenedIndicator_mono_infEdist -> thickenedIndicator_mono_infEDist Also renames some instances.