Documentation Verification Report

MetricSeparated

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

Statistics

Metric	Count
Definitions `AreSeparated`, `IsSeparated`	2
Theorems `comm`, `disjoint`, `empty_left`, `empty_right`, `finite_iUnion_left`, `finite_iUnion_left_iff`, `finite_iUnion_right_iff`, `finset_iUnion_left`, `finset_iUnion_left_iff`, `finset_iUnion_right`, `finset_iUnion_right_iff`, `mono`, `mono_left`, `mono_right`, `subset_compl_right`, `union_left`, `union_left_iff`, `union_right`, `union_right_iff`, `anti`, `empty`, `image_antilipschitz`, `insert`, `of_subsingleton`, `singleton`, `subset`, `isSeparated_iff_setRelIsSeparated`, `isSeparated_insert`, `isSeparated_insert_of_notMem`, `isSeparated_zero`, `isSeparated`	31
Total	33

Metric

Definitions

Name	Category	Theorems
`AreSeparated` 📖	MathDef	9 math math: `AreSeparated.finset_iUnion_right_iff`, `AreSeparated.empty_left`, `AreSeparated.comm`, `AreSeparated.finite_iUnion_right_iff`, `AreSeparated.empty_right`, `AreSeparated.finite_iUnion_left_iff`, `AreSeparated.union_left_iff`, `AreSeparated.union_right_iff`, `AreSeparated.finset_iUnion_left_iff`
`IsSeparated` 📖	MathDef	11 math math: `isSeparated_insert_of_notMem`, `isSeparated_iff_setRelIsSeparated`, `IsSeparated.of_subsingleton`, `isSeparated_insert`, `IsSeparated.singleton`, `isSeparated_maximalSeparatedSet`, `isSeparated_zero`, `IsSeparated.empty`, `Set.Subsingleton.isSeparated`, `Delone.DeloneSet.isSeparated_packingRadius`, `exists_set_encard_eq_packingNumber`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSeparated_iff_setRelIsSeparated` 📖	mathematical	—	`IsSeparated` `SetRel.IsSeparated` `setOf` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	—
`isSeparated_insert` 📖	mathematical	—	`IsSeparated` `Set` `Set.instInsert` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	`Set.pairwise_insert_of_symmetric` `PseudoEMetricSpace.edist_comm`
`isSeparated_insert_of_notMem` 📖	mathematical	`Set` `Set.instMembership`	`IsSeparated` `Set.instInsert` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	`Set.pairwise_insert_of_symmetric_of_notMem` `PseudoEMetricSpace.edist_comm`
`isSeparated_zero` 📖	mathematical	—	`IsSeparated` `EMetricSpace.toPseudoEMetricSpace` `ENNReal` `instZeroENNReal`	—	—

Metric.AreSeparated

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comm` 📖	mathematical	—	`Metric.AreSeparated`	—	`symm`
`disjoint` 📖	mathematical	`Metric.AreSeparated`	`Disjoint` `Set` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	`Set.disjoint_left` `PseudoEMetricSpace.edist_self` `ENNReal.instCanonicallyOrderedAdd`
`empty_left` 📖	mathematical	—	`Metric.AreSeparated` `Set` `Set.instEmptyCollection`	—	`one_ne_zero` `NeZero.charZero_one` `ENNReal.instCharZero`
`empty_right` 📖	mathematical	—	`Metric.AreSeparated` `Set` `Set.instEmptyCollection`	—	`symm` `empty_left`
`finite_iUnion_left` 📖	mathematical	`Metric.AreSeparated`	`Set.iUnion` `Set` `Set.instMembership`	—	`finite_iUnion_left_iff`
`finite_iUnion_left_iff` 📖	mathematical	—	`Metric.AreSeparated` `Set.iUnion` `Set` `Set.instMembership`	—	`Set.Finite.induction_on` `Set.iUnion_congr_Prop` `Set.iUnion_of_empty` `instIsEmptyFalse` `Set.iUnion_empty` `Set.biUnion_insert` `Set.forall_mem_insert` `union_left_iff`
`finite_iUnion_right_iff` 📖	mathematical	—	`Metric.AreSeparated` `Set.iUnion` `Set` `Set.instMembership`	—	`comm` `finite_iUnion_left_iff`
`finset_iUnion_left` 📖	mathematical	`Metric.AreSeparated`	`Set.iUnion` `Finset` `Finset.instMembership`	—	`finset_iUnion_left_iff`
`finset_iUnion_left_iff` 📖	mathematical	—	`Metric.AreSeparated` `Set.iUnion` `Finset` `Finset.instMembership`	—	`finite_iUnion_left_iff` `Finset.finite_toSet`
`finset_iUnion_right` 📖	mathematical	`Metric.AreSeparated`	`Set.iUnion` `Finset` `Finset.instMembership`	—	`finset_iUnion_right_iff`
`finset_iUnion_right_iff` 📖	mathematical	—	`Metric.AreSeparated` `Set.iUnion` `Finset` `Finset.instMembership`	—	`finite_iUnion_right_iff` `Finset.finite_toSet`
`mono` 📖	—	`Set` `Set.instHasSubset` `Metric.AreSeparated`	—	—	—
`mono_left` 📖	—	`Metric.AreSeparated` `Set` `Set.instHasSubset`	—	—	`mono` `Set.Subset.rfl`
`mono_right` 📖	—	`Metric.AreSeparated` `Set` `Set.instHasSubset`	—	—	`mono` `Set.Subset.rfl`
`subset_compl_right` 📖	mathematical	`Metric.AreSeparated`	`Set` `Set.instHasSubset` `Compl.compl` `Set.instCompl`	—	`Disjoint.le_bot` `disjoint`
`union_left` 📖	mathematical	`Metric.AreSeparated`	`Set` `Set.instUnion`	—	`pos_iff_ne_zero` `ENNReal.instCanonicallyOrderedAdd` `lt_min` `LE.le.trans` `min_le_left` `min_le_right`
`union_left_iff` 📖	mathematical	—	`Metric.AreSeparated` `Set` `Set.instUnion`	—	`mono_left` `Set.subset_union_left` `Set.subset_union_right` `union_left`
`union_right` 📖	mathematical	`Metric.AreSeparated`	`Set` `Set.instUnion`	—	`symm` `union_left`
`union_right_iff` 📖	mathematical	—	`Metric.AreSeparated` `Set` `Set.instUnion`	—	`comm` `union_left_iff`

Metric.IsSeparated

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`anti` 📖	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Metric.IsSeparated`	—	—	`Set.Pairwise.mono'` `LE.le.trans_lt`
`empty` 📖	mathematical	—	`Metric.IsSeparated` `Set` `Set.instEmptyCollection`	—	`Set.pairwise_empty`
`image_antilipschitz` 📖	mathematical	`Metric.IsSeparated` `ENNReal.ofNNReal` `AntilipschitzWith` `NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal`	`NNReal.instDiv` `Set.image`	—	`lt_of_lt_of_le` `mul_comm` `ENNReal.div_lt_of_lt_mul` `ENNReal.coe_div` `LT.lt.ne'`
`insert` 📖	mathematical	`Metric.IsSeparated` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `EDist.edist` `PseudoEMetricSpace.toEDist`	`Set` `Set.instInsert`	—	`Metric.isSeparated_insert`
`of_subsingleton` 📖	mathematical	`Set.Subsingleton`	`Metric.IsSeparated`	—	`Set.Subsingleton.pairwise`
`singleton` 📖	mathematical	—	`Metric.IsSeparated` `Set` `Set.instSingletonSet`	—	`Set.pairwise_singleton`
`subset` 📖	—	`Set` `Set.instHasSubset` `Metric.IsSeparated`	—	—	`Set.Pairwise.mono`

Set.Subsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSeparated` 📖	mathematical	`Set.Subsingleton`	`Metric.IsSeparated`	—	`Metric.IsSeparated.of_subsingleton`

---

← Back to Index