Commit 2023-04-07 13:27 76215d08

View on Github →

feat: port Topology.MetricSpace.HausdorffDistance (#3313)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Real/ENNReal.lean

modified theorem ENNReal.toNNReal_mono

added theorem ENNReal.toReal_le_add'

added theorem ENNReal.toReal_le_add

added theorem ENNReal.toReal_mono'

added theorem ENNReal.toReal_ofNat

Modified Mathlib/Mathport/Rename.lean

Modified Mathlib/Topology/MetricSpace/Basic.lean

added theorem Metric.ediam_eq_top_iff_unbounded

modified theorem Metric.ediam_of_unbounded

Created Mathlib/Topology/MetricSpace/HausdorffDistance.lean

added theorem Disjoint.exists_cthickenings

added theorem Disjoint.exists_thickenings

added theorem EMetric.continuous_infEdist

added theorem EMetric.disjoint_closedBall_of_lt_infEdist

added theorem EMetric.edist_le_infEdist_add_ediam

added theorem EMetric.empty_or_nonempty_of_hausdorffEdist_ne_top

added theorem EMetric.exists_edist_lt_of_hausdorffEdist_lt

added theorem EMetric.exists_pos_forall_lt_edist

added theorem EMetric.exists_real_pos_lt_infEdist_of_not_mem_closure

added theorem EMetric.hausdorffEdist_closure

added theorem EMetric.hausdorffEdist_closure₁

added theorem EMetric.hausdorffEdist_closure₂

added theorem EMetric.hausdorffEdist_comm

added theorem EMetric.hausdorffEdist_empty

added theorem EMetric.hausdorffEdist_image

added theorem EMetric.hausdorffEdist_le_ediam

added theorem EMetric.hausdorffEdist_le_of_infEdist

added theorem EMetric.hausdorffEdist_le_of_mem_edist

added theorem EMetric.hausdorffEdist_self

added theorem EMetric.hausdorffEdist_self_closure

added theorem EMetric.hausdorffEdist_triangle

added theorem EMetric.hausdorffEdist_zero_iff_closure_eq_closure

added theorem EMetric.hausdorffEdist_zero_iff_eq_of_closed

added def EMetric.infEdist

added theorem EMetric.infEdist_anti

added theorem EMetric.infEdist_closure

added theorem EMetric.infEdist_closure_pos_iff_not_mem_closure

added theorem EMetric.infEdist_empty

added theorem EMetric.infEdist_image

added theorem EMetric.infEdist_le_edist_add_infEdist

added theorem EMetric.infEdist_le_edist_of_mem

added theorem EMetric.infEdist_le_hausdorffEdist_of_mem

added theorem EMetric.infEdist_le_infEdist_add_edist

added theorem EMetric.infEdist_le_infEdist_add_hausdorffEdist

added theorem EMetric.infEdist_lt_iff

added theorem EMetric.infEdist_pos_iff_not_mem_closure

added theorem EMetric.infEdist_singleton

added theorem EMetric.infEdist_union

added theorem EMetric.infEdist_unionᵢ

added theorem EMetric.infEdist_zero_of_mem

added theorem EMetric.le_infEdist

added theorem EMetric.mem_closure_iff_infEdist_zero

added theorem EMetric.mem_iff_infEdist_zero_of_closed

added theorem EMetric.nonempty_of_hausdorffEdist_ne_top

added theorem IsClosed.exists_infDist_eq_dist

added theorem IsClosed.hausdorffDist_zero_iff_eq

added theorem IsClosed.mem_iff_infDist_zero

added theorem IsClosed.not_mem_iff_infDist_pos

added theorem IsCompact.cthickening_eq_bUnion_closedBall

added theorem IsCompact.exists_cthickening_subset_open

added theorem IsCompact.exists_infDist_eq_dist

added theorem IsCompact.exists_infEdist_eq_edist

added theorem IsCompact.exists_thickening_subset_open

added theorem IsOpen.exists_unionᵢ_isClosed

added theorem Metric.Bounded.cthickening

added theorem Metric.ball_infDist_compl_subset

added theorem Metric.ball_infDist_subset_compl

added theorem Metric.ball_subset_thickening

added theorem Metric.closedBall_subset_cthickening

added theorem Metric.closedBall_subset_cthickening_singleton

added theorem Metric.closure_eq_interᵢ_cthickening'

added theorem Metric.closure_eq_interᵢ_cthickening

added theorem Metric.closure_eq_interᵢ_thickening'

added theorem Metric.closure_eq_interᵢ_thickening

added theorem Metric.closure_subset_cthickening

added theorem Metric.closure_subset_thickening

added theorem Metric.closure_thickening_subset_cthickening

added theorem Metric.coe_infNndist

added theorem Metric.continuous_infDist_pt

added theorem Metric.continuous_infNndist_pt

added def Metric.cthickening

added theorem Metric.cthickening_closure

added theorem Metric.cthickening_cthickening_subset

added theorem Metric.cthickening_empty

added theorem Metric.cthickening_eq_bunionᵢ_closedBall

added theorem Metric.cthickening_eq_interᵢ_cthickening'

added theorem Metric.cthickening_eq_interᵢ_cthickening

added theorem Metric.cthickening_eq_interᵢ_thickening''

added theorem Metric.cthickening_eq_interᵢ_thickening'

added theorem Metric.cthickening_eq_interᵢ_thickening

added theorem Metric.cthickening_eq_preimage_infEdist

added theorem Metric.cthickening_max_zero

added theorem Metric.cthickening_mem_nhdsSet

added theorem Metric.cthickening_mono

added theorem Metric.cthickening_of_nonpos

added theorem Metric.cthickening_singleton

added theorem Metric.cthickening_subset_of_subset

added theorem Metric.cthickening_subset_thickening'

added theorem Metric.cthickening_subset_thickening

added theorem Metric.cthickening_subset_unionᵢ_closedBall_of_lt

added theorem Metric.cthickening_thickening_subset

added theorem Metric.cthickening_union

added theorem Metric.cthickening_zero

added theorem Metric.diam_cthickening_le

added theorem Metric.diam_thickening_le

added theorem Metric.disjoint_ball_infDist

added theorem Metric.disjoint_closedBall_of_lt_infDist

added theorem Metric.dist_le_infDist_add_diam

added theorem Metric.ediam_cthickening_le

added theorem Metric.ediam_thickening_le

added theorem Metric.exists_dist_lt_of_hausdorffDist_lt'

added theorem Metric.exists_dist_lt_of_hausdorffDist_lt

added theorem Metric.exists_mem_closure_infDist_eq_dist

added theorem Metric.frontier_cthickening_disjoint

added theorem Metric.frontier_cthickening_subset

added theorem Metric.frontier_thickening_disjoint

added theorem Metric.frontier_thickening_subset

added theorem Metric.hasBasis_nhdsSet_cthickening

added theorem Metric.hasBasis_nhdsSet_thickening

added def Metric.hausdorffDist

added theorem Metric.hausdorffDist_closure

added theorem Metric.hausdorffDist_closure₁

added theorem Metric.hausdorffDist_closure₂

added theorem Metric.hausdorffDist_comm

added theorem Metric.hausdorffDist_empty'

added theorem Metric.hausdorffDist_empty

added theorem Metric.hausdorffDist_image

added theorem Metric.hausdorffDist_le_diam

added theorem Metric.hausdorffDist_le_of_infDist

added theorem Metric.hausdorffDist_le_of_mem_dist

added theorem Metric.hausdorffDist_nonneg

added theorem Metric.hausdorffDist_self_closure

added theorem Metric.hausdorffDist_self_zero

added theorem Metric.hausdorffDist_triangle'

added theorem Metric.hausdorffDist_triangle

added theorem Metric.hausdorffDist_zero_iff_closure_eq_closure

added theorem Metric.hausdorffEdist_ne_top_of_nonempty_of_bounded

added def Metric.infDist

added theorem Metric.infDist_closure

added theorem Metric.infDist_empty

added theorem Metric.infDist_image

added theorem Metric.infDist_inter_closedBall_of_mem

added theorem Metric.infDist_le_dist_of_mem

added theorem Metric.infDist_le_hausdorffDist_of_mem

added theorem Metric.infDist_le_infDist_add_dist

added theorem Metric.infDist_le_infDist_add_hausdorffDist

added theorem Metric.infDist_le_infDist_of_subset

added theorem Metric.infDist_lt_iff

added theorem Metric.infDist_nonneg

added theorem Metric.infDist_singleton

added theorem Metric.infDist_zero_of_mem

added theorem Metric.infDist_zero_of_mem_closure

added theorem Metric.infEdist_eq_top_iff

added theorem Metric.infEdist_le_infEdist_cthickening_add

added theorem Metric.infEdist_le_infEdist_thickening_add

added theorem Metric.infEdist_ne_top

added def Metric.infNndist

added theorem Metric.isClosed_cthickening

added theorem Metric.isOpen_thickening

added theorem Metric.lipschitz_infDist_pt

added theorem Metric.lipschitz_infNndist_pt

added theorem Metric.mem_closure_iff_infDist_zero

added theorem Metric.mem_cthickening_iff

added theorem Metric.mem_cthickening_of_dist_le

added theorem Metric.mem_cthickening_of_edist_le

added theorem Metric.mem_thickening_iff

added theorem Metric.mem_thickening_iff_exists_edist_lt

added theorem Metric.mem_thickening_iff_infDist_lt

added theorem Metric.mem_thickening_iff_infEdist_lt

added theorem Metric.not_mem_of_dist_lt_infDist

added theorem Metric.self_subset_cthickening

added theorem Metric.self_subset_thickening

added def Metric.thickening

added theorem Metric.thickening_closure

added theorem Metric.thickening_cthickening_subset

added theorem Metric.thickening_empty

added theorem Metric.thickening_eq_bUnion_ball

added theorem Metric.thickening_eq_preimage_infEdist

added theorem Metric.thickening_mem_nhdsSet

added theorem Metric.thickening_mono

added theorem Metric.thickening_of_nonpos

added theorem Metric.thickening_singleton

added theorem Metric.thickening_subset_cthickening

added theorem Metric.thickening_subset_cthickening_of_le

added theorem Metric.thickening_subset_interior_cthickening

added theorem Metric.thickening_subset_of_subset

added theorem Metric.thickening_thickening_subset

added theorem Metric.thickening_union

added theorem Metric.thickening_unionᵢ

added theorem Metric.uniformContinuous_infDist_pt

added theorem Metric.uniformContinuous_infNndist_pt

Modified scripts/start_port.sh