HausdorffDistance

📁 Source: Mathlib/Topology/MetricSpace/HausdorffDistance.lean

Statistics

Metric	Count
Definitions `hausdorffEdist`, `infEdist`, `hausdorffDist`, `hausdorffEDist`, `infDist`, `infEDist`, `infNndist`	7
Theorems `continuous_infEdist`, `disjoint_closedBall_of_lt_infEdist`, `edist_le_infEdist_add_ediam`, `empty_or_nonempty_of_hausdorffEdist_ne_top`, `exists_edist_lt_of_hausdorffEdist_lt`, `exists_pos_forall_lt_edist`, `exists_real_pos_lt_infEdist_of_notMem_closure`, `hausdorffEdist_closure`, `hausdorffEdist_closure₁`, `hausdorffEdist_closure₂`, `hausdorffEdist_comm`, `hausdorffEdist_def`, `hausdorffEdist_empty`, `hausdorffEdist_iUnion_le`, `hausdorffEdist_image`, `hausdorffEdist_le_ediam`, `hausdorffEdist_le_of_infEdist`, `hausdorffEdist_le_of_mem_edist`, `hausdorffEdist_prod_le`, `hausdorffEdist_self`, `hausdorffEdist_self_closure`, `hausdorffEdist_singleton`, `hausdorffEdist_triangle`, `hausdorffEdist_union_le`, `hausdorffEdist_zero_iff_closure_eq_closure`, `hausdorffEdist_zero_iff_eq_of_closed`, `infEdist_anti`, `infEdist_biUnion`, `infEdist_closure`, `infEdist_closure_pos_iff_notMem_closure`, `infEdist_empty`, `infEdist_iUnion`, `infEdist_image`, `infEdist_le_edist_add_infEdist`, `infEdist_le_edist_of_mem`, `infEdist_le_hausdorffEdist_of_mem`, `infEdist_le_infEdist_add_edist`, `infEdist_le_infEdist_add_hausdorffEdist`, `infEdist_lt_iff`, `infEdist_pos_iff_notMem_closure`, `infEdist_prod`, `infEdist_singleton`, `infEdist_smul`, `infEdist_union`, `infEdist_vadd`, `infEdist_zero_of_mem`, `le_infEdist`, `mem_closure_iff_infEdist_zero`, `mem_iff_infEdist_zero_of_closed`, `nonempty_of_hausdorffEdist_ne_top`, `exists_infDist_eq_dist`, `hausdorffDist_zero_iff_eq`, `hausdorffEDist_zero_iff`, `mem_iff_infDist_zero`, `notMem_iff_infDist_pos`, `exists_infDist_eq_dist`, `exists_infEDist_eq_edist`, `exists_infEdist_eq_edist`, `exists_iUnion_isClosed`, `ball_infDist_compl_subset`, `ball_infDist_subset_compl`, `coe_infNndist`, `continuousAt_inv_infDist_pt`, `continuous_infDist_pt`, `continuous_infEDist`, `continuous_infNndist_pt`, `disjoint_ball_infDist`, `disjoint_closedBall_of_lt_infDist`, `disjoint_closedEBall_of_lt_infEDist`, `dist_le_infDist_add_diam`, `edist_le_infEDist_add_ediam`, `empty_or_nonempty_of_hausdorffEDist_ne_top`, `exists_dist_lt_of_hausdorffDist_lt`, `exists_dist_lt_of_hausdorffDist_lt'`, `exists_edist_lt_of_hausdorffEDist_lt`, `exists_mem_closure_infDist_eq_dist`, `exists_pos_forall_lt_edist`, `exists_real_pos_lt_infEDist_of_notMem_closure`, `hausdorffDist_closure`, `hausdorffDist_closure₁`, `hausdorffDist_closure₂`, `hausdorffDist_comm`, `hausdorffDist_empty`, `hausdorffDist_empty'`, `hausdorffDist_image`, `hausdorffDist_le_diam`, `hausdorffDist_le_of_infDist`, `hausdorffDist_le_of_mem_dist`, `hausdorffDist_nonneg`, `hausdorffDist_self_closure`, `hausdorffDist_self_zero`, `hausdorffDist_singleton`, `hausdorffDist_triangle`, `hausdorffDist_triangle'`, `hausdorffDist_zero_iff_closure_eq_closure`, `hausdorffEDist_closure`, `hausdorffEDist_closure_left`, `hausdorffEDist_closure_right`, `hausdorffEDist_comm`, `hausdorffEDist_def`, `hausdorffEDist_empty`, `hausdorffEDist_iUnion_le`, `hausdorffEDist_image`, `hausdorffEDist_le_ediam`, `hausdorffEDist_le_of_infEDist`, `hausdorffEDist_le_of_mem_edist`, `hausdorffEDist_ne_top_of_nonempty_of_bounded`, `hausdorffEDist_prod_le`, `hausdorffEDist_self`, `hausdorffEDist_self_closure`, `hausdorffEDist_singleton`, `hausdorffEDist_triangle`, `hausdorffEDist_union_le`, `hausdorffEDist_zero_iff_closure_eq_closure`, `hausdorffEdist_ne_top_of_nonempty_of_bounded`, `infDist_closure`, `infDist_empty`, `infDist_eq_iInf`, `infDist_image`, `infDist_inter_closedBall_of_mem`, `infDist_le_dist_of_mem`, `infDist_le_hausdorffDist_of_mem`, `infDist_le_infDist_add_dist`, `infDist_le_infDist_add_hausdorffDist`, `infDist_le_infDist_of_subset`, `infDist_lt_iff`, `infDist_nonneg`, `infDist_pos_iff_notMem_closure`, `infDist_singleton`, `infDist_zero_of_mem`, `infDist_zero_of_mem_closure`, `infEDist_anti`, `infEDist_biUnion`, `infEDist_closure`, `infEDist_closure_pos_iff_notMem_closure`, `infEDist_empty`, `infEDist_eq_top_iff`, `infEDist_iUnion`, `infEDist_image`, `infEDist_le_edist_add_infEDist`, `infEDist_le_edist_of_mem`, `infEDist_le_hausdorffEDist_of_mem`, `infEDist_le_infEDist_add_edist`, `infEDist_le_infEDist_add_hausdorffEDist`, `infEDist_lt_iff`, `infEDist_ne_top`, `infEDist_pos_iff_notMem_closure`, `infEDist_prod`, `infEDist_singleton`, `infEDist_smul`, `infEDist_union`, `infEDist_vadd`, `infEDist_zero_of_mem`, `infEdist_eq_top_iff`, `infEdist_ne_top`, `isGLB_infDist`, `le_infDist`, `le_infEDist`, `lipschitz_infDist_pt`, `lipschitz_infNndist_pt`, `mem_closure_iff_infDist_zero`, `mem_closure_iff_infEDist_zero`, `mem_iff_infEDist_zero_of_closed`, `nonempty_of_hausdorffEDist_ne_top`, `notMem_of_dist_lt_infDist`, `uniformContinuous_infDist_pt`, `uniformContinuous_infNndist_pt`	167
Total	174

EMetric

Definitions

Name	Category	Theorems
`hausdorffEdist` 📖	CompOp	—
`infEdist` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_infEdist` 📖	mathematical	—	`Continuous` `ENNReal` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `ENNReal.instTopologicalSpace` `Metric.infEDist`	—	`Metric.continuous_infEDist`
`disjoint_closedBall_of_lt_infEdist` 📖	mathematical	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Metric.infEDist`	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Metric.closedEBall`	—	`Metric.disjoint_closedEBall_of_lt_infEDist`
`edist_le_infEdist_add_ediam` 📖	mathematical	`Set` `Set.instMembership`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `EDist.edist` `PseudoEMetricSpace.toEDist` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `Metric.infEDist` `Metric.ediam`	—	`Metric.edist_le_infEDist_add_ediam`
`empty_or_nonempty_of_hausdorffEdist_ne_top` 📖	mathematical	—	`Set` `Set.instEmptyCollection` `Set.Nonempty`	—	`Metric.empty_or_nonempty_of_hausdorffEDist_ne_top`
`exists_edist_lt_of_hausdorffEdist_lt` 📖	mathematical	`Set` `Set.instMembership` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Metric.hausdorffEDist`	`EDist.edist` `PseudoEMetricSpace.toEDist`	—	`Metric.exists_edist_lt_of_hausdorffEDist_lt`
`exists_pos_forall_lt_edist` 📖	mathematical	`IsCompact` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal` `ENNReal` `ENNReal.instPartialOrder` `ENNReal.ofNNReal` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	`Metric.exists_pos_forall_lt_edist`
`exists_real_pos_lt_infEdist_of_notMem_closure` 📖	mathematical	`Set` `Set.instMembership` `closure` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	`Real` `Real.instLT` `Real.instZero` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ENNReal.ofReal` `Metric.infEDist`	—	`Metric.exists_real_pos_lt_infEDist_of_notMem_closure`
`hausdorffEdist_closure` 📖	mathematical	—	`Metric.hausdorffEDist` `closure` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	—	`Metric.hausdorffEDist_closure`
`hausdorffEdist_closure₁` 📖	mathematical	—	`Metric.hausdorffEDist` `closure` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	—	`Metric.hausdorffEDist_closure_left`
`hausdorffEdist_closure₂` 📖	mathematical	—	`Metric.hausdorffEDist` `closure` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	—	`Metric.hausdorffEDist_closure_right`
`hausdorffEdist_comm` 📖	mathematical	—	`Metric.hausdorffEDist`	—	`Metric.hausdorffEDist_comm`
`hausdorffEdist_def` 📖	mathematical	—	`Metric.hausdorffEDist` `ENNReal` `ENNReal.instMax` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `Set` `Set.instMembership` `Metric.infEDist`	—	`Metric.hausdorffEDist_def`
`hausdorffEdist_empty` 📖	mathematical	`Set.Nonempty`	`Metric.hausdorffEDist` `Set` `Set.instEmptyCollection` `Top.top` `ENNReal` `instTopENNReal`	—	`Metric.hausdorffEDist_empty`
`hausdorffEdist_iUnion_le` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Metric.hausdorffEDist` `Set.iUnion` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder`	—	`Metric.hausdorffEDist_iUnion_le`
`hausdorffEdist_image` 📖	mathematical	`Isometry`	`Metric.hausdorffEDist` `Set.image`	—	`Metric.hausdorffEDist_image`
`hausdorffEdist_le_ediam` 📖	mathematical	`Set.Nonempty`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Metric.hausdorffEDist` `Metric.ediam` `Set` `Set.instUnion`	—	`Metric.hausdorffEDist_le_ediam`
`hausdorffEdist_le_of_infEdist` 📖	mathematical	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Metric.infEDist`	`Metric.hausdorffEDist`	—	`Metric.hausdorffEDist_le_of_infEDist`
`hausdorffEdist_le_of_mem_edist` 📖	mathematical	`Set` `Set.instMembership` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `EDist.edist` `PseudoEMetricSpace.toEDist`	`Metric.hausdorffEDist`	—	`Metric.hausdorffEDist_le_of_mem_edist`
`hausdorffEdist_prod_le` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Metric.hausdorffEDist` `Prod.pseudoEMetricSpaceMax` `SProd.sprod` `Set` `Set.instSProd` `ENNReal.instMax`	—	`Metric.hausdorffEDist_prod_le`
`hausdorffEdist_self` 📖	mathematical	—	`Metric.hausdorffEDist` `ENNReal` `instZeroENNReal`	—	`Metric.hausdorffEDist_self`
`hausdorffEdist_self_closure` 📖	mathematical	—	`Metric.hausdorffEDist` `closure` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `ENNReal` `instZeroENNReal`	—	`Metric.hausdorffEDist_self_closure`
`hausdorffEdist_singleton` 📖	mathematical	—	`Metric.hausdorffEDist` `Set` `Set.instSingletonSet` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	`Metric.hausdorffEDist_singleton`
`hausdorffEdist_triangle` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Metric.hausdorffEDist` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring`	—	`Metric.hausdorffEDist_triangle`
`hausdorffEdist_union_le` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Metric.hausdorffEDist` `Set` `Set.instUnion` `ENNReal.instMax`	—	`Metric.hausdorffEDist_union_le`
`hausdorffEdist_zero_iff_closure_eq_closure` 📖	mathematical	—	`Metric.hausdorffEDist` `ENNReal` `instZeroENNReal` `closure` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	—	`Metric.hausdorffEDist_zero_iff_closure_eq_closure`
`hausdorffEdist_zero_iff_eq_of_closed` 📖	mathematical	—	`Metric.hausdorffEDist` `ENNReal` `instZeroENNReal`	—	`IsClosed.hausdorffEDist_zero_iff`
`infEdist_anti` 📖	mathematical	`Set` `Set.instHasSubset`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Metric.infEDist`	—	`Metric.infEDist_anti`
`infEdist_biUnion` 📖	mathematical	—	`Metric.infEDist` `Set.iUnion` `Set` `Set.instMembership` `iInf` `ENNReal` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder`	—	`Metric.infEDist_biUnion`
`infEdist_closure` 📖	mathematical	—	`Metric.infEDist` `closure` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	—	`Metric.infEDist_closure`
`infEdist_closure_pos_iff_notMem_closure` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal` `Metric.infEDist` `closure` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `Set` `Set.instMembership`	—	`Metric.infEDist_closure_pos_iff_notMem_closure`
`infEdist_empty` 📖	mathematical	—	`Metric.infEDist` `Set` `Set.instEmptyCollection` `Top.top` `ENNReal` `instTopENNReal`	—	`Metric.infEDist_empty`
`infEdist_iUnion` 📖	mathematical	—	`Metric.infEDist` `Set.iUnion` `iInf` `ENNReal` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder`	—	`Metric.infEDist_iUnion`
`infEdist_image` 📖	mathematical	`Isometry`	`Metric.infEDist` `Set.image`	—	`Metric.infEDist_image`
`infEdist_le_edist_add_infEdist` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Metric.infEDist` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	`Metric.infEDist_le_edist_add_infEDist`
`infEdist_le_edist_of_mem` 📖	mathematical	`Set` `Set.instMembership`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Metric.infEDist` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	`Metric.infEDist_le_edist_of_mem`
`infEdist_le_hausdorffEdist_of_mem` 📖	mathematical	`Set` `Set.instMembership`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Metric.infEDist` `Metric.hausdorffEDist`	—	`Metric.infEDist_le_hausdorffEDist_of_mem`
`infEdist_le_infEdist_add_edist` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Metric.infEDist` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	`Metric.infEDist_le_infEDist_add_edist`
`infEdist_le_infEdist_add_hausdorffEdist` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Metric.infEDist` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `Metric.hausdorffEDist`	—	`Metric.infEDist_le_infEDist_add_hausdorffEDist`
`infEdist_lt_iff` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Metric.infEDist` `Set` `Set.instMembership` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	`Metric.infEDist_lt_iff`
`infEdist_pos_iff_notMem_closure` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal` `Metric.infEDist` `Set` `Set.instMembership` `closure` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	—	`Metric.infEDist_pos_iff_notMem_closure`
`infEdist_prod` 📖	mathematical	—	`Metric.infEDist` `Prod.pseudoEMetricSpaceMax` `SProd.sprod` `Set` `Set.instSProd` `ENNReal` `ENNReal.instMax`	—	`Metric.infEDist_prod`
`infEdist_singleton` 📖	mathematical	—	`Metric.infEDist` `Set` `Set.instSingletonSet` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	`Metric.infEDist_singleton`
`infEdist_smul` 📖	mathematical	—	`Metric.infEDist` `Set` `Set.smulSet`	—	`Metric.infEDist_smul`
`infEdist_union` 📖	mathematical	—	`Metric.infEDist` `Set` `Set.instUnion` `ENNReal` `ENNReal.instMin`	—	`Metric.infEDist_union`
`infEdist_vadd` 📖	mathematical	—	`Metric.infEDist` `HVAdd.hVAdd` `instHVAdd` `Set` `Set.vaddSet`	—	`Metric.infEDist_vadd`
`infEdist_zero_of_mem` 📖	mathematical	`Set` `Set.instMembership`	`Metric.infEDist` `ENNReal` `instZeroENNReal`	—	`Metric.infEDist_zero_of_mem`
`le_infEdist` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Metric.infEDist` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	`Metric.le_infEDist`
`mem_closure_iff_infEdist_zero` 📖	mathematical	—	`Set` `Set.instMembership` `closure` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `Metric.infEDist` `ENNReal` `instZeroENNReal`	—	`Metric.mem_closure_iff_infEDist_zero`
`mem_iff_infEdist_zero_of_closed` 📖	mathematical	—	`Set` `Set.instMembership` `Metric.infEDist` `ENNReal` `instZeroENNReal`	—	`Metric.mem_iff_infEDist_zero_of_closed`
`nonempty_of_hausdorffEdist_ne_top` 📖	—	`Set.Nonempty`	—	—	`Metric.nonempty_of_hausdorffEDist_ne_top`

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_infDist_eq_dist` 📖	mathematical	`Set.Nonempty`	`Set` `Set.instMembership` `Metric.infDist` `Dist.dist` `PseudoMetricSpace.toDist`	—	`Metric.infDist_inter_closedBall_of_mem` `IsCompact.inter_left` `ProperSpace.isCompact_closedBall` `Metric.mem_closedBall` `le_rfl` `IsCompact.exists_infDist_eq_dist`
`hausdorffDist_zero_iff_eq` 📖	mathematical	—	`Metric.hausdorffDist` `Real` `Real.instZero`	—	`hausdorffEDist_zero_iff`
`hausdorffEDist_zero_iff` 📖	mathematical	—	`Metric.hausdorffEDist` `ENNReal` `instZeroENNReal`	—	`Metric.hausdorffEDist_zero_iff_closure_eq_closure` `closure_eq`
`mem_iff_infDist_zero` 📖	mathematical	`Set.Nonempty`	`Set` `Set.instMembership` `Metric.infDist` `Real` `Real.instZero`	—	`Metric.mem_closure_iff_infDist_zero` `closure_eq`
`notMem_iff_infDist_pos` 📖	mathematical	`Set.Nonempty`	`Set` `Set.instMembership` `Real` `Real.instLT` `Real.instZero` `Metric.infDist`	—	`mem_iff_infDist_zero` `LE.le.lt_iff_ne'` `Metric.infDist_nonneg`

IsCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_infDist_eq_dist` 📖	mathematical	`IsCompact` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Set.Nonempty`	`Set` `Set.instMembership` `Metric.infDist` `Dist.dist` `PseudoMetricSpace.toDist`	—	`exists_infEDist_eq_edist` `Metric.infDist.eq_1` `dist_edist`
`exists_infEDist_eq_edist` 📖	mathematical	`IsCompact` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `Set.Nonempty`	`Set` `Set.instMembership` `Metric.infEDist` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	`Continuous.edist` `continuous_const` `continuous_id'` `exists_isMinOn` `instClosedIicTopology` `OrderTopology.to_orderClosedTopology` `ENNReal.instOrderTopology` `Continuous.continuousOn` `le_antisymm` `Metric.infEDist_le_edist_of_mem` `Metric.le_infEDist`
`exists_infEdist_eq_edist` 📖	mathematical	`IsCompact` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `Set.Nonempty`	`Set` `Set.instMembership` `Metric.infEDist` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	`exists_infEDist_eq_edist`

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_iUnion_isClosed` 📖	mathematical	`IsOpen` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	`IsClosed` `Set` `Set.instHasSubset` `Set.iUnion` `Monotone` `Nat.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra`	—	`exists_between` `ENNReal.instDenselyOrdered` `zero_lt_one` `IsOrderedRing.toZeroLEOneClass` `ENNReal.instIsOrderedRing` `NeZero.charZero_one` `ENNReal.instCharZero` `LT.lt.ne'` `LT.lt.trans_le` `ENNReal.pow_pos` `Metric.infEDist_zero_of_mem` `IsClosed.preimage` `Metric.continuous_infEDist` `isClosed_Ici` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `ENNReal.instOrderTopology` `Set.Subset.antisymm` `ENNReal.instCanonicallyOrderedAdd` `Metric.mem_iff_infEDist_zero_of_closed` `isClosed_compl` `ENNReal.tendsto_pow_atTop_nhds_zero_of_lt_one` `Filter.Eventually.exists` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `tendsto_order` `LT.lt.le` `le_trans` `pow_le_pow_right_of_le_one'` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid`

Metric

Definitions

Name	Category	Theorems
`hausdorffDist` 📖	CompOp	26 math math: `hausdorffDist_empty'`, `GromovHausdorff.hausdorffDist_optimal`, `hausdorffDist_le_of_mem_dist`, `hausdorffDist_triangle`, `hausdorffDist_self_closure`, `hausdorffDist_zero_iff_closure_eq_closure`, `hausdorffDist_triangle'`, `hausdorffDist_empty`, `GromovHausdorff.ghDist_le_hausdorffDist`, `hausdorffDist_self_zero`, `hausdorffDist_comm`, `GromovHausdorff.ghDist_eq_hausdorffDist`, `hausdorffDist_le_diam`, `GromovHausdorff.hausdorffDist_optimal_le_HD`, `hausdorffDist_closure₂`, `hausdorffDist_closure`, `hausdorffDist_image`, `IsClosed.hausdorffDist_zero_iff_eq`, `infDist_le_infDist_add_hausdorffDist`, `ConvexBody.hausdorffDist_coe`, `hausdorffDist_singleton`, `infDist_le_hausdorffDist_of_mem`, `hausdorffDist_le_of_infDist`, `hausdorffDist_nonneg`, `hausdorffDist_closure₁`, `NonemptyCompacts.dist_eq`
`hausdorffEDist` 📖	CompOp	49 math math: `EMetric.hausdorffEdist_iUnion_le`, `hausdorffEDist_closure`, `hausdorffEDist_def`, `hausdorffEDist_iUnion_le`, `EMetric.hausdorffEdist_empty`, `hausdorffEDist_le_of_mem_edist`, `TopologicalSpace.Compacts.edist_eq`, `EMetric.hausdorffEdist_comm`, `hausdorffEDist_le_of_mem_hausdorffEntourage`, `hausdorffEDist_closure_right`, `hausdorffEDist_self_closure`, `hausdorffEDist_image`, `EMetric.infEdist_le_hausdorffEdist_of_mem`, `hausdorffEDist_le_of_infEDist`, `infEDist_le_hausdorffEDist_of_mem`, `hausdorffEDist_le_ediam`, `EMetric.hausdorffEdist_self`, `EMetric.hausdorffEdist_le_ediam`, `EMetric.hausdorffEdist_image`, `EMetric.hausdorffEdist_le_of_mem_edist`, `TopologicalSpace.Closeds.edist_eq`, `hausdorffEDist_empty`, `hausdorffEDist_self`, `EMetric.infEdist_le_infEdist_add_hausdorffEdist`, `EMetric.hausdorffEdist_le_of_mem_hausdorffEntourage`, `IsClosed.hausdorffEDist_zero_iff`, `hausdorffEDist_zero_iff_closure_eq_closure`, `hausdorffEDist_prod_le`, `hausdorffEDist_comm`, `hausdorffEDist_closure_left`, `EMetric.hausdorffEdist_union_le`, `EMetric.hausdorffEdist_zero_iff_closure_eq_closure`, `hausdorffEDist_triangle`, `infEDist_le_infEDist_add_hausdorffEDist`, `EMetric.hausdorffEdist_zero_iff_eq_of_closed`, `EMetric.hausdorffEdist_triangle`, `EMetric.hausdorffEdist_prod_le`, `hausdorffEDist_union_le`, `hausdorffEDist_singleton`, `EMetric.hausdorffEdist_def`, `EMetric.hausdorffEdist_le_of_infEdist`, `EMetric.hausdorffEdist_closure`, `ConvexBody.hausdorffEDist_coe`, `ConvexBody.hausdorffEdist_coe`, `EMetric.Closeds.edist_eq`, `EMetric.hausdorffEdist_self_closure`, `EMetric.hausdorffEdist_singleton`, `EMetric.hausdorffEdist_closure₂`, `EMetric.hausdorffEdist_closure₁`
`infDist` 📖	CompOp	51 math math: `disjoint_ball_infDist`, `QuotientGroup.norm_mk`, `infDist_le_dist_of_mem`, `IsCompact.exists_infDist_eq_dist`, `TopologicalSpace.Opens.CompleteCopy.dist_eq`, `IsClosed.mem_iff_infDist_zero`, `infDist_image`, `continuousAt_inv_infDist_pt`, `ball_infDist_compl_subset`, `mem_closure_iff_infDist_zero`, `ball_infDist_subset_compl`, `infDist_inter_closedBall_of_mem`, `QuotientAddGroup.norm_eq_infDist`, `QuotientAddGroup.norm_mk`, `uniformContinuous_infDist_Hausdorff_dist`, `dist_le_infDist_add_diam`, `infDist_zero_of_mem`, `infDist_closure`, `infDist_empty`, `le_infDist`, `infDist_singleton`, `infDist_le_infDist_of_subset`, `infDist_smul₀`, `mem_thickening_iff_infDist_lt`, `EuclideanGeometry.Sphere.IsTangent.infDist_eq_radius`, `Measurable.infDist`, `coe_infNndist`, `infDist_lt_iff`, `EuclideanGeometry.dist_orthogonalProjection_eq_infDist`, `infDist_le_infDist_add_dist`, `continuous_infDist_pt`, `lipschitz_infDist_pt`, `infDist_pos_iff_notMem_closure`, `QuotientGroup.norm_eq_infDist`, `lipschitz_infDist`, `IsClosed.exists_infDist_eq_dist`, `infDist_le_infDist_add_hausdorffDist`, `lipschitz_infDist_set`, `IsCompact.exists_mem_frontier_infDist_compl_eq_dist`, `infDist_zero_of_mem_closure`, `closedBall_infDist_compl_subset_closure`, `exists_mem_closure_infDist_eq_dist`, `infDist_eq_iInf`, `isGLB_infDist`, `infDist_le_hausdorffDist_of_mem`, `measurable_infDist`, `infDist_nonneg`, `uniformContinuous_infDist_pt`, `EuclideanGeometry.Sphere.infDist_eq_radius_iff_isTangent`, `IsClosed.notMem_iff_infDist_pos`, `exists_mem_frontier_infDist_compl_eq_dist`
`infEDist` 📖	CompOp	91 math math: `EMetric.infEdist_union`, `infEDist_vadd`, `infEdist_inv`, `EMetric.le_infEdist`, `hausdorffEDist_def`, `mem_thickening_iff_infEDist_lt`, `infEdist_thickening`, `mem_cthickening_iff`, `infEDist_le_edist_of_mem`, `EMetric.infEdist_pos_iff_notMem_closure`, `infEDist_neg_neg`, `infEDist_le_infEDist_add_edist`, `cthickening_eq_preimage_infEdist`, `infEdist_le_infEdist_thickening_add`, `thickening_eq_preimage_infEDist`, `EMetric.infEdist_smul`, `EMetric.infEdist_empty`, `measurable_infEDist`, `EMetric.mem_closure_iff_infEdist_zero`, `EMetric.infEdist_le_hausdorffEdist_of_mem`, `infEDist_le_hausdorffEDist_of_mem`, `EMetric.infEdist_closure_pos_iff_notMem_closure`, `infEDist_smul₀`, `Measurable.infEdist`, `EMetric.infEdist_image`, `EMetric.infEdist_anti`, `EMetric.infEdist_singleton`, `EMetric.infEdist_vadd`, `frontier_thickening_subset`, `measurable_infEdist`, `infEDist_neg`, `EMetric.infEdist_biUnion`, `cthickening_eq_preimage_infEDist`, `infEdist_smul₀`, `le_infEDist`, `mem_closure_iff_infEDist_zero`, `EMetric.infEdist_zero_of_mem`, `infEDist_union`, `EMetric.infEdist_le_infEdist_add_hausdorffEdist`, `edist_le_infEDist_add_ediam`, `EMetric.infEdist_le_edist_add_infEdist`, `infEdist_inv_inv`, `infEDist_closure_pos_iff_notMem_closure`, `EMetric.infEdist_iUnion`, `TopologicalSpace.Closeds.continuous_infEDist`, `infEDist_anti`, `EMetric.edist_le_infEdist_add_ediam`, `infEdist_eq_top_iff`, `EMetric.infEdist_closure`, `infEDist_prod`, `infEDist_thickening`, `infEdist_le_infEdist_cthickening_add`, `EMetric.infEdist_le_edist_of_mem`, `infEDist_iUnion`, `infEdist_cthickening`, `infEDist_image`, `infEDist_singleton`, `mem_thickening_iff_infEdist_lt`, `infEDist_cthickening`, `infEDist_le_infEDist_thickening_add`, `infEDist_le_infEDist_add_hausdorffEDist`, `infEDist_empty`, `infEDist_closure`, `EMetric.infEdist_lt_iff`, `infEDist_eq_top_iff`, `EMetric.infEdist_prod`, `EMetric.infEdist_le_infEdist_add_edist`, `continuous_infEDist`, `EMetric.hausdorffEdist_def`, `IsCompact.exists_infEdist_eq_edist`, `EMetric.mem_iff_infEdist_zero_of_closed`, `infEDist_le_infEDist_cthickening_add`, `infEdist_neg`, `frontier_cthickening_subset`, `infEDist_zero_of_mem`, `IsCompact.exists_infEDist_eq_edist`, `infEDist_inv_inv`, `EMetric.continuous_infEdist`, `infEdist_neg_neg`, `mem_iff_infEDist_zero_of_closed`, `infEDist_lt_iff`, `infEDist_smul`, `infEDist_inv`, `exists_real_pos_lt_infEDist_of_notMem_closure`, `Measurable.infEDist`, `EMetric.exists_real_pos_lt_infEdist_of_notMem_closure`, `infEDist_biUnion`, `EMetric.continuous_infEdist_hausdorffEdist`, `infEDist_le_edist_add_infEDist`, `thickening_eq_preimage_infEdist`, `infEDist_pos_iff_notMem_closure`
`infNndist` 📖	CompOp	7 math math: `uniformContinuous_infNndist_pt`, `EuclideanGeometry.dist_orthogonalProjection_eq_infNndist`, `coe_infNndist`, `continuous_infNndist_pt`, `measurable_infNndist`, `lipschitz_infNndist_pt`, `Measurable.infNndist`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ball_infDist_compl_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `ball` `infDist` `Compl.compl` `Set.instCompl`	—	`LE.le.trans_eq` `ball_infDist_subset_compl` `compl_compl`
`ball_infDist_subset_compl` 📖	mathematical	—	`Set` `Set.instHasSubset` `ball` `infDist` `Compl.compl` `Set.instCompl`	—	`Disjoint.subset_compl_right` `disjoint_ball_infDist`
`coe_infNndist` 📖	mathematical	—	`NNReal.toReal` `infNndist` `infDist`	—	—
`continuousAt_inv_infDist_pt` 📖	mathematical	`Set` `Set.instMembership` `closure` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace`	`ContinuousAt` `Real` `Real.pseudoMetricSpace` `Real.instInv` `infDist`	—	`Set.eq_empty_or_nonempty` `infDist_empty` `ContinuousAt.inv₀` `IsTopologicalDivisionRing.toContinuousInv₀` `instIsTopologicalDivisionRingReal` `Continuous.continuousAt` `continuous_infDist_pt` `mem_closure_iff_infDist_zero`
`continuous_infDist_pt` 📖	mathematical	—	`Continuous` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `infDist`	—	`UniformContinuous.continuous` `uniformContinuous_infDist_pt`
`continuous_infEDist` 📖	mathematical	—	`Continuous` `ENNReal` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `ENNReal.instTopologicalSpace` `infEDist`	—	`continuous_of_le_add_edist` `one_mul`
`continuous_infNndist_pt` 📖	mathematical	—	`Continuous` `NNReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `NNReal.instTopologicalSpace` `infNndist`	—	`UniformContinuous.continuous` `uniformContinuous_infNndist_pt`
`disjoint_ball_infDist` 📖	mathematical	—	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `ball` `infDist`	—	`Set.disjoint_left` `notMem_of_dist_lt_infDist` `mem_ball'`
`disjoint_closedBall_of_lt_infDist` 📖	mathematical	`Real` `Real.instLT` `infDist`	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `closedBall`	—	`Disjoint.mono_left` `closedBall_subset_ball` `disjoint_ball_infDist`
`disjoint_closedEBall_of_lt_infEDist` 📖	mathematical	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `infEDist`	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `closedEBall`	—	`Set.disjoint_left` `lt_irrefl` `infEDist_le_edist_of_mem` `PseudoEMetricSpace.edist_comm` `mem_closedEBall`
`dist_le_infDist_add_diam` 📖	mathematical	`Bornology.IsBounded` `PseudoMetricSpace.toBornology` `Set` `Set.instMembership`	`Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `Real.instAdd` `infDist` `diam`	—	`infDist.eq_1` `diam.eq_1` `dist_edist` `ENNReal.toReal_le_add` `edist_le_infEDist_add_ediam` `infEDist_ne_top` `Bornology.IsBounded.ediam_ne_top`
`edist_le_infEDist_add_ediam` 📖	mathematical	`Set` `Set.instMembership`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `EDist.edist` `PseudoEMetricSpace.toEDist` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `infEDist` `ediam`	—	`ENNReal.iInf_add` `le_iInf₂` `PseudoEMetricSpace.edist_triangle` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `le_rfl` `edist_le_ediam_of_mem`
`empty_or_nonempty_of_hausdorffEDist_ne_top` 📖	mathematical	—	`Set` `Set.instEmptyCollection` `Set.Nonempty`	—	`Set.eq_empty_or_nonempty` `nonempty_of_hausdorffEDist_ne_top` `hausdorffEDist_comm`
`exists_dist_lt_of_hausdorffDist_lt` 📖	mathematical	`Set` `Set.instMembership` `Real` `Real.instLT` `hausdorffDist`	`Dist.dist` `PseudoMetricSpace.toDist`	—	`lt_of_le_of_lt` `hausdorffDist_nonneg` `ENNReal.toReal_lt_toReal` `ENNReal.ofReal_ne_top` `ENNReal.toReal_ofReal` `le_of_lt` `hausdorffDist.eq_1` `exists_edist_lt_of_hausdorffEDist_lt` `ENNReal.ofReal_lt_ofReal_iff` `edist_dist`
`exists_dist_lt_of_hausdorffDist_lt'` 📖	mathematical	`Set` `Set.instMembership` `Real` `Real.instLT` `hausdorffDist`	`Dist.dist` `PseudoMetricSpace.toDist`	—	`dist_comm` `exists_dist_lt_of_hausdorffDist_lt` `hausdorffDist_comm` `hausdorffEDist_comm`
`exists_edist_lt_of_hausdorffEDist_lt` 📖	mathematical	`Set` `Set.instMembership` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `hausdorffEDist`	`EDist.edist` `PseudoEMetricSpace.toEDist`	—	`infEDist_lt_iff` `infEDist_le_hausdorffEDist_of_mem`
`exists_mem_closure_infDist_eq_dist` 📖	mathematical	`Set.Nonempty`	`Set` `Set.instMembership` `closure` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `infDist` `Dist.dist` `PseudoMetricSpace.toDist`	—	`infDist_closure` `IsClosed.exists_infDist_eq_dist` `isClosed_closure` `Set.Nonempty.closure`
`exists_pos_forall_lt_edist` 📖	mathematical	`IsCompact` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal` `ENNReal` `ENNReal.instPartialOrder` `ENNReal.ofNNReal` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	`Set.eq_empty_or_nonempty` `LinearOrderedCommMonoidWithZero.toZeroLeOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `NNReal.instIsStrictOrderedRing` `instIsEmptyFalse` `IsCompact.exists_isMinOn` `instClosedIicTopology` `OrderTopology.to_orderClosedTopology` `ENNReal.instOrderTopology` `Continuous.continuousOn` `continuous_infEDist` `pos_iff_ne_zero` `ENNReal.instCanonicallyOrderedAdd` `Disjoint.le_bot` `mem_iff_infEDist_zero_of_closed` `ENNReal.lt_iff_exists_nnreal_btwn` `ENNReal.coe_pos` `LT.lt.trans_le` `le_infEDist`
`exists_real_pos_lt_infEDist_of_notMem_closure` 📖	mathematical	`Set` `Set.instMembership` `closure` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	`Real` `Real.instLT` `Real.instZero` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ENNReal.ofReal` `infEDist`	—	`ENNReal.lt_iff_exists_real_btwn` `infEDist_pos_iff_notMem_closure` `ENNReal.ofReal_pos`
`hausdorffDist_closure` 📖	mathematical	—	`hausdorffDist` `closure` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace`	—	`hausdorffEDist_closure_right` `hausdorffEDist_closure_left`
`hausdorffDist_closure₁` 📖	mathematical	—	`hausdorffDist` `closure` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace`	—	`hausdorffEDist_closure_left`
`hausdorffDist_closure₂` 📖	mathematical	—	`hausdorffDist` `closure` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace`	—	`hausdorffEDist_closure_right`
`hausdorffDist_comm` 📖	mathematical	—	`hausdorffDist`	—	`hausdorffEDist_comm`
`hausdorffDist_empty` 📖	mathematical	—	`hausdorffDist` `Set` `Set.instEmptyCollection` `Real` `Real.instZero`	—	`Set.eq_empty_or_nonempty` `hausdorffDist_self_zero` `hausdorffEDist_empty`
`hausdorffDist_empty'` 📖	mathematical	—	`hausdorffDist` `Set` `Set.instEmptyCollection` `Real` `Real.instZero`	—	`hausdorffDist_comm` `hausdorffDist_empty`
`hausdorffDist_image` 📖	mathematical	`Isometry` `PseudoMetricSpace.toPseudoEMetricSpace`	`hausdorffDist` `Set.image`	—	`hausdorffEDist_image`
`hausdorffDist_le_diam` 📖	mathematical	`Set.Nonempty` `Bornology.IsBounded` `PseudoMetricSpace.toBornology`	`Real` `Real.instLE` `hausdorffDist` `diam` `Set` `Set.instUnion`	—	`hausdorffDist_le_of_mem_dist` `diam_nonneg` `dist_le_diam_of_mem` `Bornology.IsBounded.union` `Set.subset_union_left` `Set.subset_union_right`
`hausdorffDist_le_of_infDist` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `infDist`	`hausdorffDist`	—	`Set.eq_empty_or_nonempty` `hausdorffDist_empty'` `hausdorffDist_empty` `hausdorffEDist_le_of_infEDist` `ENNReal.le_ofReal_iff_toReal_le` `infEDist_ne_top` `ENNReal.toReal_le_of_le_ofReal`
`hausdorffDist_le_of_mem_dist` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `Set` `Set.instMembership` `Dist.dist` `PseudoMetricSpace.toDist`	`hausdorffDist`	—	`hausdorffDist_le_of_infDist` `le_trans` `infDist_le_dist_of_mem`
`hausdorffDist_nonneg` 📖	mathematical	—	`Real` `Real.instLE` `Real.instZero` `hausdorffDist`	—	—
`hausdorffDist_self_closure` 📖	mathematical	—	`hausdorffDist` `closure` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real` `Real.instZero`	—	`hausdorffEDist_self_closure`
`hausdorffDist_self_zero` 📖	mathematical	—	`hausdorffDist` `Real` `Real.instZero`	—	`hausdorffEDist_self`
`hausdorffDist_singleton` 📖	mathematical	—	`hausdorffDist` `Set` `Set.instSingletonSet` `Dist.dist` `PseudoMetricSpace.toDist`	—	`hausdorffDist.eq_1` `hausdorffEDist_singleton` `dist_edist`
`hausdorffDist_triangle` 📖	mathematical	—	`Real` `Real.instLE` `hausdorffDist` `Real.instAdd`	—	`ENNReal.toReal_le_add'` `hausdorffEDist_triangle` `not_imp_not` `ne_top_of_le_ne_top` `ENNReal.add_ne_top` `hausdorffEDist_comm`
`hausdorffDist_triangle'` 📖	mathematical	—	`Real` `Real.instLE` `hausdorffDist` `Real.instAdd`	—	`hausdorffDist_triangle` `hausdorffEDist_comm` `hausdorffDist_comm` `add_comm`
`hausdorffDist_zero_iff_closure_eq_closure` 📖	mathematical	—	`hausdorffDist` `Real` `Real.instZero` `closure` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace`	—	—
`hausdorffEDist_closure` 📖	mathematical	—	`hausdorffEDist` `closure` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	—	`hausdorffEDist_closure_right` `hausdorffEDist_closure_left`
`hausdorffEDist_closure_left` 📖	mathematical	—	`hausdorffEDist` `closure` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	—	`le_antisymm` `hausdorffEDist_triangle` `hausdorffEDist_comm` `hausdorffEDist_self_closure` `zero_add`
`hausdorffEDist_closure_right` 📖	mathematical	—	`hausdorffEDist` `closure` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	—	`hausdorffEDist_comm` `hausdorffEDist_closure_left`
`hausdorffEDist_comm` 📖	mathematical	—	`hausdorffEDist`	—	`hausdorffEDist_def` `sup_comm`
`hausdorffEDist_def` 📖	mathematical	—	`hausdorffEDist` `ENNReal` `ENNReal.instMax` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `Set` `Set.instMembership` `infEDist`	—	—
`hausdorffEDist_empty` 📖	mathematical	`Set.Nonempty`	`hausdorffEDist` `Set` `Set.instEmptyCollection` `Top.top` `ENNReal` `instTopENNReal`	—	`infEDist_le_hausdorffEDist_of_mem` `infEDist_empty`
`hausdorffEDist_iUnion_le` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `hausdorffEDist` `Set.iUnion` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder`	—	`hausdorffEDist_def` `iSup_iUnion` `infEDist_iUnion` `LE.le.trans` `iInf_le` `le_iSup_of_le` `le_max_of_le_left` `le_iSup₂_of_le` `le_rfl` `le_max_of_le_right`
`hausdorffEDist_image` 📖	mathematical	`Isometry`	`hausdorffEDist` `Set.image`	—	`hausdorffEDist_def` `iSup_image` `iSup_congr_Prop` `infEDist_image`
`hausdorffEDist_le_ediam` 📖	mathematical	`Set.Nonempty`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `hausdorffEDist` `ediam` `Set` `Set.instUnion`	—	`hausdorffEDist_le_of_mem_edist` `edist_le_ediam_of_mem` `Set.subset_union_left` `Set.subset_union_right`
`hausdorffEDist_le_of_infEDist` 📖	mathematical	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `infEDist`	`hausdorffEDist`	—	`hausdorffEDist_def`
`hausdorffEDist_le_of_mem_edist` 📖	mathematical	`Set` `Set.instMembership` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `EDist.edist` `PseudoEMetricSpace.toEDist`	`hausdorffEDist`	—	`hausdorffEDist_le_of_infEDist` `le_trans` `infEDist_le_edist_of_mem`
`hausdorffEDist_ne_top_of_nonempty_of_bounded` 📖	—	`Set.Nonempty` `Bornology.IsBounded` `PseudoMetricSpace.toBornology`	—	—	`Bornology.IsBounded.subset_closedBall` `hausdorffEDist_le_of_mem_edist` `le_trans` `le_max_left` `edist_dist` `ENNReal.ofReal_le_ofReal_iff` `dist_nonneg` `le_max_right` `ne_top_of_le_ne_top` `ENNReal.ofReal_ne_top`
`hausdorffEDist_prod_le` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `hausdorffEDist` `Prod.pseudoEMetricSpaceMax` `SProd.sprod` `Set` `Set.instSProd` `ENNReal.instMax`	—	`le_of_forall_ge` `hausdorffEDist_def` `iSup_congr_Prop` `infEDist_prod`
`hausdorffEDist_self` 📖	mathematical	—	`hausdorffEDist` `ENNReal` `instZeroENNReal`	—	`hausdorffEDist_def` `sup_idem` `infEDist_zero_of_mem`
`hausdorffEDist_self_closure` 📖	mathematical	—	`hausdorffEDist` `closure` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `ENNReal` `instZeroENNReal`	—	`hausdorffEDist_zero_iff_closure_eq_closure` `closure_closure`
`hausdorffEDist_singleton` 📖	mathematical	—	`hausdorffEDist` `Set` `Set.instSingletonSet` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	`hausdorffEDist_def` `iSup_singleton` `infEDist_singleton` `PseudoEMetricSpace.edist_comm` `max_self`
`hausdorffEDist_triangle` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `hausdorffEDist` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring`	—	`hausdorffEDist_def` `infEDist_le_infEDist_add_hausdorffEDist` `le_imp_le_of_le_of_le` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `infEDist_le_hausdorffEDist_of_mem` `le_refl` `hausdorffEDist_comm` `add_comm`
`hausdorffEDist_union_le` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `hausdorffEDist` `Set` `Set.instUnion` `ENNReal.instMax`	—	`Set.union_eq_iUnion` `sup_eq_iSup` `hausdorffEDist_iUnion_le`
`hausdorffEDist_zero_iff_closure_eq_closure` 📖	mathematical	—	`hausdorffEDist` `ENNReal` `instZeroENNReal` `closure` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	—	`hausdorffEDist_def` `Set.instReflSubset` `Set.instAntisymmSubset` `IsClosed.closure_subset_iff` `isClosed_closure`
`hausdorffEdist_ne_top_of_nonempty_of_bounded` 📖	—	`Set.Nonempty` `Bornology.IsBounded` `PseudoMetricSpace.toBornology`	—	—	`hausdorffEDist_ne_top_of_nonempty_of_bounded`
`infDist_closure` 📖	mathematical	—	`infDist` `closure` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace`	—	`infEDist_closure`
`infDist_empty` 📖	mathematical	—	`infDist` `Set` `Set.instEmptyCollection` `Real` `Real.instZero`	—	`infEDist_empty`
`infDist_eq_iInf` 📖	mathematical	—	`infDist` `iInf` `Real` `Set.Elem` `Real.instInfSet` `Dist.dist` `PseudoMetricSpace.toDist` `Set` `Set.instMembership`	—	`infDist.eq_1` `infEDist.eq_1` `iInf_subtype'` `ENNReal.toReal_iInf` `edist_ne_top` `dist_edist`
`infDist_image` 📖	mathematical	`Isometry` `PseudoMetricSpace.toPseudoEMetricSpace`	`infDist` `Set.image`	—	`infEDist_image`
`infDist_inter_closedBall_of_mem` 📖	mathematical	`Set` `Set.instMembership`	`infDist` `Set.instInter` `closedBall` `Dist.dist` `PseudoMetricSpace.toDist`	—	`mem_closedBall` `le_rfl` `le_antisymm` `not_lt` `infDist_lt_iff` `le_or_gt` `LT.lt.not_ge` `infDist_le_dist_of_mem` `LT.lt.trans` `dist_comm` `infDist_le_infDist_of_subset` `Set.inter_subset_left`
`infDist_le_dist_of_mem` 📖	mathematical	`Set` `Set.instMembership`	`Real` `Real.instLE` `infDist` `Dist.dist` `PseudoMetricSpace.toDist`	—	`dist_edist` `infDist.eq_1` `ENNReal.toReal_mono` `edist_ne_top` `infEDist_le_edist_of_mem`
`infDist_le_hausdorffDist_of_mem` 📖	mathematical	`Set` `Set.instMembership`	`Real` `Real.instLE` `infDist` `hausdorffDist`	—	`ENNReal.toReal_mono` `infEDist_le_hausdorffEDist_of_mem`
`infDist_le_infDist_add_dist` 📖	mathematical	—	`Real` `Real.instLE` `infDist` `Real.instAdd` `Dist.dist` `PseudoMetricSpace.toDist`	—	`infDist.eq_1` `dist_edist` `ENNReal.toReal_le_add'` `infEDist_le_infEDist_add_edist` `edist_ne_top`
`infDist_le_infDist_add_hausdorffDist` 📖	mathematical	—	`Real` `Real.instLE` `infDist` `Real.instAdd` `hausdorffDist`	—	`ENNReal.toReal_le_add'` `infEDist_le_infEDist_add_hausdorffEDist` `infEDist_eq_top_iff` `Set.not_nonempty_iff_eq_empty` `nonempty_of_hausdorffEDist_ne_top` `hausdorffEDist_comm`
`infDist_le_infDist_of_subset` 📖	mathematical	`Set` `Set.instHasSubset` `Set.Nonempty`	`Real` `Real.instLE` `infDist`	—	`ENNReal.toReal_mono` `infEDist_ne_top` `infEDist_anti`
`infDist_lt_iff` 📖	mathematical	`Set.Nonempty`	`Real` `Real.instLT` `infDist` `Set` `Set.instMembership` `Dist.dist` `PseudoMetricSpace.toDist`	—	`le_infDist`
`infDist_nonneg` 📖	mathematical	—	`Real` `Real.instLE` `Real.instZero` `infDist`	—	`ENNReal.toReal_nonneg`
`infDist_pos_iff_notMem_closure` 📖	mathematical	`Set.Nonempty`	`Set` `Set.instMembership` `closure` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real` `Real.instLT` `Real.instZero` `infDist`	—	`Iff.not` `mem_closure_iff_infDist_zero` `LE.le.lt_iff_ne'` `infDist_nonneg`
`infDist_singleton` 📖	mathematical	—	`infDist` `Set` `Set.instSingletonSet` `Dist.dist` `PseudoMetricSpace.toDist`	—	`infEDist_singleton` `dist_edist`
`infDist_zero_of_mem` 📖	mathematical	`Set` `Set.instMembership`	`infDist` `Real` `Real.instZero`	—	`infEDist_zero_of_mem`
`infDist_zero_of_mem_closure` 📖	mathematical	`Set` `Set.instMembership` `closure` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace`	`infDist` `Real` `Real.instZero`	—	`infDist_closure` `infDist_zero_of_mem`
`infEDist_anti` 📖	mathematical	`Set` `Set.instHasSubset`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `infEDist`	—	`iInf_le_iInf_of_subset`
`infEDist_biUnion` 📖	mathematical	—	`infEDist` `Set.iUnion` `Set` `Set.instMembership` `iInf` `ENNReal` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder`	—	`infEDist_iUnion`
`infEDist_closure` 📖	mathematical	—	`infEDist` `closure` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	—	`le_antisymm` `infEDist_anti` `subset_closure` `ENNReal.le_of_forall_pos_le_add` `Nat.instAtLeastTwoHAddOfNat` `ENNReal.instCanonicallyOrderedAdd` `NNReal.instCanonicallyOrderedAdd` `ENNReal.lt_add_right` `LT.lt.ne` `LT.lt.ne'` `infEDist_lt_iff` `EMetric.mem_closure_iff` `infEDist_le_edist_of_mem` `PseudoEMetricSpace.edist_triangle` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `le_of_lt` `add_assoc` `ENNReal.add_halves`
`infEDist_closure_pos_iff_notMem_closure` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal` `infEDist` `closure` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `Set` `Set.instMembership`	—	`infEDist_closure` `infEDist_pos_iff_notMem_closure`
`infEDist_empty` 📖	mathematical	—	`infEDist` `Set` `Set.instEmptyCollection` `Top.top` `ENNReal` `instTopENNReal`	—	`iInf_emptyset`
`infEDist_eq_top_iff` 📖	mathematical	—	`infEDist` `PseudoMetricSpace.toPseudoEMetricSpace` `Top.top` `ENNReal` `instTopENNReal` `Set` `Set.instEmptyCollection`	—	`Set.eq_empty_or_nonempty` `infEDist_empty`
`infEDist_iUnion` 📖	mathematical	—	`infEDist` `Set.iUnion` `iInf` `ENNReal` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder`	—	`iInf_iUnion`
`infEDist_image` 📖	mathematical	`Isometry`	`infEDist` `Set.image`	—	`iInf_image` `iInf_congr_Prop` `Isometry.edist_eq`
`infEDist_le_edist_add_infEDist` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `infEDist` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	`add_comm` `infEDist_le_infEDist_add_edist`
`infEDist_le_edist_of_mem` 📖	mathematical	`Set` `Set.instMembership`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `infEDist` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	`iInf₂_le`
`infEDist_le_hausdorffEDist_of_mem` 📖	mathematical	`Set` `Set.instMembership`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `infEDist` `hausdorffEDist`	—	`hausdorffEDist_def` `le_trans` `le_iSup₂` `le_sup_left`
`infEDist_le_infEDist_add_edist` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `infEDist` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	`iInf₂_mono` `LE.le.trans_eq` `PseudoEMetricSpace.edist_triangle` `add_comm` `ENNReal.iInf_add`
`infEDist_le_infEDist_add_hausdorffEDist` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `infEDist` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `hausdorffEDist`	—	`ENNReal.le_of_forall_pos_le_add` `Nat.instAtLeastTwoHAddOfNat` `NNReal.instCanonicallyOrderedAdd` `ENNReal.lt_add_right` `LT.lt.ne` `ENNReal.add_lt_top` `infEDist_lt_iff` `exists_edist_lt_of_hausdorffEDist_lt` `infEDist_le_edist_of_mem` `PseudoEMetricSpace.edist_triangle` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `LT.lt.le` `add_add_add_comm` `ENNReal.add_halves`
`infEDist_lt_iff` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `infEDist` `Set` `Set.instMembership` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	—
`infEDist_ne_top` 📖	—	`Set.Nonempty`	—	—	`ne_top_of_le_ne_top` `edist_ne_top` `infEDist_le_edist_of_mem`
`infEDist_pos_iff_notMem_closure` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal` `infEDist` `Set` `Set.instMembership` `closure` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	—	`mem_closure_iff_infEDist_zero` `pos_iff_ne_zero` `ENNReal.instCanonicallyOrderedAdd`
`infEDist_prod` 📖	mathematical	—	`infEDist` `Prod.pseudoEMetricSpaceMax` `SProd.sprod` `Set` `Set.instSProd` `ENNReal` `ENNReal.instMax`	—	`iInf_congr_Prop` `iInf_prod` `iInf_and` `iInf_sup_eq` `sup_iInf_eq`
`infEDist_singleton` 📖	mathematical	—	`infEDist` `Set` `Set.instSingletonSet` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	`iInf_singleton`
`infEDist_smul` 📖	mathematical	—	`infEDist` `Set` `Set.smulSet`	—	`infEDist_image` `IsIsometricSMul.isometry_smul`
`infEDist_union` 📖	mathematical	—	`infEDist` `Set` `Set.instUnion` `ENNReal` `ENNReal.instMin`	—	`iInf_union`
`infEDist_vadd` 📖	mathematical	—	`infEDist` `HVAdd.hVAdd` `instHVAdd` `Set` `Set.vaddSet`	—	`infEDist_image` `IsIsometricVAdd.isometry_vadd`
`infEDist_zero_of_mem` 📖	mathematical	`Set` `Set.instMembership`	`infEDist` `ENNReal` `instZeroENNReal`	—	`nonpos_iff_eq_zero` `ENNReal.instCanonicallyOrderedAdd` `infEDist_le_edist_of_mem` `PseudoEMetricSpace.edist_self`
`infEdist_eq_top_iff` 📖	mathematical	—	`infEDist` `PseudoMetricSpace.toPseudoEMetricSpace` `Top.top` `ENNReal` `instTopENNReal` `Set` `Set.instEmptyCollection`	—	`infEDist_eq_top_iff`
`infEdist_ne_top` 📖	—	`Set.Nonempty`	—	—	`infEDist_ne_top`
`isGLB_infDist` 📖	mathematical	`Set.Nonempty`	`IsGLB` `Real` `Real.instLE` `Set.image` `Dist.dist` `PseudoMetricSpace.toDist` `infDist`	—	`infDist_eq_iInf` `sInf_image'` `isGLB_csInf` `Set.Nonempty.image`
`le_infDist` 📖	mathematical	`Set.Nonempty`	`Real` `Real.instLE` `infDist` `Dist.dist` `PseudoMetricSpace.toDist`	—	`ENNReal.ofReal_le_iff_le_toReal` `infEDist_ne_top` `edist_ne_top`
`le_infEDist` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `infEDist` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	—
`lipschitz_infDist_pt` 📖	mathematical	—	`LipschitzWith` `Real` `PseudoMetricSpace.toPseudoEMetricSpace` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Real.metricSpace` `NNReal` `instOneNNReal` `infDist`	—	`LipschitzWith.of_le_add` `infDist_le_infDist_add_dist`
`lipschitz_infNndist_pt` 📖	mathematical	—	`LipschitzWith` `NNReal` `PseudoMetricSpace.toPseudoEMetricSpace` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `instMetricSpaceNNReal` `instOneNNReal` `infNndist`	—	`LipschitzWith.of_le_add` `infDist_le_infDist_add_dist`
`mem_closure_iff_infDist_zero` 📖	mathematical	`Set.Nonempty`	`Set` `Set.instMembership` `closure` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `infDist` `Real` `Real.instZero`	—	`infEDist_ne_top`
`mem_closure_iff_infEDist_zero` 📖	mathematical	—	`Set` `Set.instMembership` `closure` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `infEDist` `ENNReal` `instZeroENNReal`	—	`infEDist_closure` `infEDist_zero_of_mem` `EMetric.mem_closure_iff` `infEDist_lt_iff`
`mem_iff_infEDist_zero_of_closed` 📖	mathematical	—	`Set` `Set.instMembership` `infEDist` `ENNReal` `instZeroENNReal`	—	`mem_closure_iff_infEDist_zero` `IsClosed.closure_eq`
`nonempty_of_hausdorffEDist_ne_top` 📖	—	`Set.Nonempty`	—	—	`Set.eq_empty_or_nonempty` `hausdorffEDist_empty`
`notMem_of_dist_lt_infDist` 📖	mathematical	`Real` `Real.instLT` `Dist.dist` `PseudoMetricSpace.toDist` `infDist`	`Set` `Set.instMembership`	—	`LT.lt.not_ge` `infDist_le_dist_of_mem`
`uniformContinuous_infDist_pt` 📖	mathematical	—	`UniformContinuous` `Real` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `infDist`	—	`LipschitzWith.uniformContinuous` `lipschitz_infDist_pt`
`uniformContinuous_infNndist_pt` 📖	mathematical	—	`UniformContinuous` `NNReal` `PseudoMetricSpace.toUniformSpace` `instPseudoMetricSpaceNNReal` `infNndist`	—	`LipschitzWith.uniformContinuous` `lipschitz_infNndist_pt`

---

← Back to Index