Diam

📁 Source: Mathlib/Topology/EMetricSpace/Diam.lean

Statistics

Metric	Count
Definitions `diam`, `ediam`	2
Theorems `diam_ball`, `diam_closedBall`, `diam_empty`, `diam_eq_sSup`, `diam_eq_zero_iff`, `diam_iUnion_mem_option`, `diam_image_le_iff`, `diam_insert`, `diam_le`, `diam_le_iff`, `diam_mono`, `diam_one`, `diam_pair`, `diam_pi_le_of_le`, `diam_pos_iff`, `diam_pos_iff'`, `diam_singleton`, `diam_subsingleton`, `diam_triple`, `diam_union`, `diam_union'`, `diam_zero`, `edist_le_diam_of_mem`, `edist_le_of_diam_le`, `ediam_closedEBall_le`, `ediam_eball_le`, `ediam_empty`, `ediam_eq_sSup`, `ediam_eq_zero_iff`, `ediam_iUnion_mem_option`, `ediam_image_le_iff`, `ediam_insert`, `ediam_le`, `ediam_le_iff`, `ediam_mono`, `ediam_one`, `ediam_pair`, `ediam_pi_le_of_le`, `ediam_pos_iff`, `ediam_pos_iff'`, `ediam_singleton`, `ediam_subsingleton`, `ediam_triple`, `ediam_union_le`, `ediam_union_le_add_edist`, `ediam_zero`, `edist_le_ediam_of_mem`, `edist_le_of_ediam_le`, `ediam_eq`	49
Total	51

EMetric

Definitions

Name	Category	Theorems
`diam` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`diam_ball` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Metric.ediam` `Metric.eball` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat`	—	`Metric.ediam_eball_le`
`diam_closedBall` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Metric.ediam` `Metric.closedEBall` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat`	—	`Metric.ediam_closedEBall_le`
`diam_empty` 📖	mathematical	—	`Metric.ediam` `Set` `Set.instEmptyCollection` `ENNReal` `instZeroENNReal`	—	`Metric.ediam_empty`
`diam_eq_sSup` 📖	mathematical	—	`Metric.ediam` `SupSet.sSup` `ENNReal` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `Set.image2` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	`Metric.ediam_eq_sSup`
`diam_eq_zero_iff` 📖	mathematical	—	`Metric.ediam` `EMetricSpace.toPseudoEMetricSpace` `ENNReal` `instZeroENNReal` `Set.Subsingleton`	—	`Metric.ediam_eq_zero_iff`
`diam_iUnion_mem_option` 📖	mathematical	—	`Metric.ediam` `Set.iUnion` `iSup` `ENNReal` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder`	—	`Metric.ediam_iUnion_mem_option`
`diam_image_le_iff` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Metric.ediam` `Set.image` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	`Metric.ediam_image_le_iff`
`diam_insert` 📖	mathematical	—	`Metric.ediam` `Set` `Set.instInsert` `ENNReal` `ENNReal.instMax` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `Set.instMembership` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	`Metric.ediam_insert`
`diam_le` 📖	mathematical	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `EDist.edist` `PseudoEMetricSpace.toEDist`	`Metric.ediam`	—	`Metric.ediam_le`
`diam_le_iff` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Metric.ediam` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	`Metric.ediam_le_iff`
`diam_mono` 📖	mathematical	`Set` `Set.instHasSubset`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Metric.ediam`	—	`Metric.ediam_mono`
`diam_one` 📖	mathematical	—	`Metric.ediam` `Set` `Set.one` `ENNReal` `instZeroENNReal`	—	`Metric.ediam_one`
`diam_pair` 📖	mathematical	—	`Metric.ediam` `Set` `Set.instInsert` `Set.instSingletonSet` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	`Metric.ediam_pair`
`diam_pi_le_of_le` 📖	mathematical	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Metric.ediam`	`pseudoEMetricSpacePi` `Set.pi` `Set.univ`	—	`Metric.ediam_pi_le_of_le`
`diam_pos_iff` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal` `Metric.ediam` `EMetricSpace.toPseudoEMetricSpace` `Set.Nontrivial`	—	`Metric.ediam_pos_iff`
`diam_pos_iff'` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal` `Metric.ediam` `EMetricSpace.toPseudoEMetricSpace` `Set` `Set.instMembership`	—	`Metric.ediam_pos_iff'`
`diam_singleton` 📖	mathematical	—	`Metric.ediam` `Set` `Set.instSingletonSet` `ENNReal` `instZeroENNReal`	—	`Metric.ediam_singleton`
`diam_subsingleton` 📖	mathematical	`Set.Subsingleton`	`Metric.ediam` `ENNReal` `instZeroENNReal`	—	`Metric.ediam_subsingleton`
`diam_triple` 📖	mathematical	—	`Metric.ediam` `Set` `Set.instInsert` `Set.instSingletonSet` `ENNReal` `ENNReal.instMax` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	`Metric.ediam_triple`
`diam_union` 📖	mathematical	`Set` `Set.instMembership`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Metric.ediam` `Set.instUnion` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	`Metric.ediam_union_le_add_edist`
`diam_union'` 📖	mathematical	`Set.Nonempty` `Set` `Set.instInter`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Metric.ediam` `Set.instUnion` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring`	—	`Metric.ediam_union_le`
`diam_zero` 📖	mathematical	—	`Metric.ediam` `Set` `Set.zero` `ENNReal` `instZeroENNReal`	—	`Metric.ediam_zero`
`edist_le_diam_of_mem` 📖	mathematical	`Set` `Set.instMembership`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `EDist.edist` `PseudoEMetricSpace.toEDist` `Metric.ediam`	—	`Metric.edist_le_ediam_of_mem`
`edist_le_of_diam_le` 📖	mathematical	`Set` `Set.instMembership` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Metric.ediam`	`EDist.edist` `PseudoEMetricSpace.toEDist`	—	`Metric.edist_le_of_ediam_le`

Metric

Definitions

Name	Category	Theorems
`ediam` 📖	CompOp	111 math math: `EMetric.diam_pos_iff'`, `EMetric.diam_empty`, `Isometry.ediam_range`, `SemilinearIsometryClass.ediam_image`, `Real.ediam_eq`, `EMetric.diam_mono`, `ediam_closedEBall_le`, `LipschitzWith.ediam_image_le`, `SemilinearIsometryClass.ediam_range`, `ediam_thickening_le`, `ediam_univ_of_noncompact`, `EMetric.diam_pair`, `MeasureTheory.Measure.mkMetric_apply`, `IsCompact.uniform_oscillation`, `IsometryEquiv.ediam_univ`, `EMetric.diam_le_iff`, `ediam_triple`, `Perfect.small_diam_splitting`, `MeasureTheory.Measure.hausdorffMeasure_le_liminf_sum`, `IsometryClass.ediam_range`, `ediam_smul_le`, `ediam_zero`, `ediam_eq_top_iff_unbounded`, `Dilation.ediam_range`, `ediam_empty`, `MeasureTheory.Measure.mkMetric_le_liminf_tsum`, `ediam_closure`, `EMetric.diam_singleton`, `ediam_pos_iff'`, `EMetric.diam_insert`, `Real.ediam_Ioc`, `IsometryEquiv.ediam_preimage`, `hausdorffEDist_le_ediam`, `Snowflaking.ediam_image_ofSnowflaking`, `EMetric.diam_union'`, `ediam_one`, `EMetric.hausdorffEdist_le_ediam`, `EMetric.diam_ball`, `HolderWith.ediam_image_le`, `ediam_union_le`, `ediam_cthickening_le`, `ediam_eq_sSup`, `LipschitzOnWith.ediam_image2_le`, `LinearIsometry.ediam_image`, `EMetric.diam_le`, `EMetric.diam_closure`, `Real.volume_pi_le_prod_diam`, `edist_le_ediam_of_mem`, `ediam_eball_le`, `ediam_subsingleton`, `Snowflaking.ediam_preimage_ofSnowflaking`, `ediam_pos_iff`, `edist_le_infEDist_add_ediam`, `ediam_mono`, `IsometryEquiv.ediam_image`, `EMetric.edist_le_infEdist_add_ediam`, `ediam_smul`, `ediam_vadd`, `EMetric.edist_le_diam_of_mem`, `MeasureTheory.Measure.hausdorffMeasure_le_liminf_tsum`, `ediam_pair`, `Real.volume_le_diam`, `Isometry.ediam_image`, `EMetric.diam_pos_iff`, `EMetric.diam_image_le_iff`, `convexHull_ediam`, `Real.ediam_Ioo`, `AffineIsometry.ediam_range`, `ediam_image_le_iff`, `ediam_le`, `Real.volume_pi_le_diam_pow`, `ediam_smul₀`, `ediam_le_of_forall_dist_le`, `EMetric.diam_one`, `AffineIsometryEquiv.ediam_image`, `MeasureTheory.Measure.hausdorffMeasure_apply`, `ediam_of_unbounded`, `ediam_union_le_add_edist`, `LinearIsometry.ediam_range`, `MeasureTheory.Measure.mkMetric_le_liminf_sum`, `ediam_eq_zero_iff`, `ediam_mul_le`, `EMetric.diam_subsingleton`, `EMetric.diam_zero`, `Dilation.ediam_image`, `EMetric.diam_eq_sSup`, `HolderOnWith.ediam_image_inter_le`, `ediam_add_le`, `ediam_univ_eq_top_iff_noncompact`, `Snowflaking.ediam_preimage_toSnowflaking`, `ediam_iUnion_mem_option`, `EMetric.diam_union`, `HolderOnWith.ediam_image_le`, `EMetric.diam_triple`, `AntilipschitzWith.le_mul_ediam_image`, `EMetric.diam_eq_zero_iff`, `IsCompact.uniform_oscillationWithin`, `ediam_le_iff`, `IsometryClass.ediam_image`, `HolderOnWith.ediam_image_le_of_subset`, `ediam_singleton`, `AffineIsometry.ediam_image`, `Snowflaking.ediam_image_toSnowflaking`, `AntilipschitzWith.ediam_preimage_le`, `EMetric.diam_closedBall`, `Set.Subsingleton.ediam_eq`, `Real.ediam_Icc`, `ediam_insert`, `Real.ediam_Ico`, `LinearIsometryEquiv.ediam_image`, `EMetric.diam_iUnion_mem_option`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ediam_closedEBall_le` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ediam` `closedEBall` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat`	—	`ediam_le` `Nat.instAtLeastTwoHAddOfNat` `edist_triangle_right` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `two_mul`
`ediam_eball_le` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ediam` `eball` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat`	—	`le_trans` `Nat.instAtLeastTwoHAddOfNat` `ediam_mono` `eball_subset_closedEBall` `ediam_closedEBall_le`
`ediam_empty` 📖	mathematical	—	`ediam` `Set` `Set.instEmptyCollection` `ENNReal` `instZeroENNReal`	—	`ediam_subsingleton` `Set.subsingleton_empty`
`ediam_eq_sSup` 📖	mathematical	—	`ediam` `SupSet.sSup` `ENNReal` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `Set.image2` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	`sSup_image2`
`ediam_eq_zero_iff` 📖	mathematical	—	`ediam` `EMetricSpace.toPseudoEMetricSpace` `ENNReal` `instZeroENNReal` `Set.Subsingleton`	—	`edist_le_zero` `edist_le_ediam_of_mem` `ediam_subsingleton`
`ediam_iUnion_mem_option` 📖	mathematical	—	`ediam` `Set.iUnion` `iSup` `ENNReal` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder`	—	`Set.iUnion_congr_Prop` `Set.iUnion_of_empty` `instIsEmptyFalse` `Set.iUnion_empty` `ediam_empty` `iSup_congr_Prop` `iSup_neg` `bot_eq_zero'` `ENNReal.instCanonicallyOrderedAdd` `ENNReal.iSup_zero` `Set.iUnion_iUnion_eq_right` `iSup_iSup_eq_right`
`ediam_image_le_iff` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ediam` `Set.image` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	—
`ediam_insert` 📖	mathematical	—	`ediam` `Set` `Set.instInsert` `ENNReal` `ENNReal.instMax` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `Set.instMembership` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	`eq_of_forall_ge_iff` `PseudoEMetricSpace.edist_comm` `PseudoEMetricSpace.edist_self` `ENNReal.instCanonicallyOrderedAdd`
`ediam_le` 📖	mathematical	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `EDist.edist` `PseudoEMetricSpace.toEDist`	`ediam`	—	`ediam_le_iff`
`ediam_le_iff` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ediam` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	—
`ediam_mono` 📖	mathematical	`Set` `Set.instHasSubset`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ediam`	—	`ediam_le` `edist_le_ediam_of_mem`
`ediam_one` 📖	mathematical	—	`ediam` `Set` `Set.one` `ENNReal` `instZeroENNReal`	—	`ediam_singleton`
`ediam_pair` 📖	mathematical	—	`ediam` `Set` `Set.instInsert` `Set.instSingletonSet` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	`ediam_insert` `iSup_congr_Prop` `iSup_iSup_eq_left` `ediam_singleton` `sup_of_le_left` `ENNReal.instCanonicallyOrderedAdd`
`ediam_pi_le_of_le` 📖	mathematical	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ediam`	`pseudoEMetricSpacePi` `Set.pi` `Set.univ`	—	`ediam_le` `edist_pi_le_iff` `ediam_le_iff` `Set.mem_univ_pi`
`ediam_pos_iff` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal` `ediam` `EMetricSpace.toPseudoEMetricSpace` `Set.Nontrivial`	—	`ENNReal.instCanonicallyOrderedAdd`
`ediam_pos_iff'` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal` `ediam` `EMetricSpace.toPseudoEMetricSpace` `Set` `Set.instMembership`	—	—
`ediam_singleton` 📖	mathematical	—	`ediam` `Set` `Set.instSingletonSet` `ENNReal` `instZeroENNReal`	—	`ediam_subsingleton` `Set.subsingleton_singleton`
`ediam_subsingleton` 📖	mathematical	`Set.Subsingleton`	`ediam` `ENNReal` `instZeroENNReal`	—	`nonpos_iff_eq_zero` `ENNReal.instCanonicallyOrderedAdd` `ediam_le` `le_rfl` `PseudoEMetricSpace.edist_self`
`ediam_triple` 📖	mathematical	—	`ediam` `Set` `Set.instInsert` `Set.instSingletonSet` `ENNReal` `ENNReal.instMax` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	`ediam_insert` `iSup_insert` `iSup_singleton` `ediam_singleton` `ENNReal.max_zero_right`
`ediam_union_le` 📖	mathematical	`Set.Nonempty` `Set` `Set.instInter`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ediam` `Set.instUnion` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring`	—	`PseudoEMetricSpace.edist_self` `add_zero` `ediam_union_le_add_edist`
`ediam_union_le_add_edist` 📖	mathematical	`Set` `Set.instMembership`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ediam` `Set.instUnion` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	`edist_triangle4` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `add_le_add_left` `edist_le_ediam_of_mem` `ediam_le` `Set.mem_union` `le_self_add` `ENNReal.instCanonicallyOrderedAdd` `add_assoc` `PseudoEMetricSpace.edist_comm` `le_add_self`
`ediam_zero` 📖	mathematical	—	`ediam` `Set` `Set.zero` `ENNReal` `instZeroENNReal`	—	`ediam_singleton`
`edist_le_ediam_of_mem` 📖	mathematical	`Set` `Set.instMembership`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `EDist.edist` `PseudoEMetricSpace.toEDist` `ediam`	—	`edist_le_of_ediam_le` `le_rfl`
`edist_le_of_ediam_le` 📖	mathematical	`Set` `Set.instMembership` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ediam`	`EDist.edist` `PseudoEMetricSpace.toEDist`	—	`ediam_le_iff`

Set.Subsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ediam_eq` 📖	mathematical	`Set.Subsingleton`	`Metric.ediam` `ENNReal` `instZeroENNReal`	—	`Metric.ediam_subsingleton`

---

← Back to Index