CoveringNumbers

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

Statistics

Metric	Count
Definitions `coveringNumber`, `externalCoveringNumber`, `maximalSeparatedSet`, `minimalCover`, `packingNumber`	5
Theorems `coveringNumber_image`, `coveringNumber_image'`, `coveringNumber_le_encard`, `externalCoveringNumber_le_encard`, `encard_le_packingNumber`, `coveringNumber_anti`, `coveringNumber_empty`, `coveringNumber_eq_one_of_ediam_le`, `coveringNumber_eq_zero`, `coveringNumber_le_encard_self`, `coveringNumber_le_one_of_ediam_le`, `coveringNumber_le_packingNumber`, `coveringNumber_pos_iff`, `coveringNumber_singleton`, `coveringNumber_subset_le`, `coveringNumber_two_mul_le_externalCoveringNumber`, `coveringNumber_zero`, `encard_le_of_isSeparated`, `encard_maximalSeparatedSet`, `encard_minimalCover`, `exists_set_encard_eq_coveringNumber`, `exists_set_encard_eq_packingNumber`, `externalCoveringNumber_anti`, `externalCoveringNumber_empty`, `externalCoveringNumber_eq_one_of_ediam_le`, `externalCoveringNumber_eq_zero`, `externalCoveringNumber_le_coveringNumber`, `externalCoveringNumber_le_encard_self`, `externalCoveringNumber_le_one_of_ediam_le`, `externalCoveringNumber_mono_set`, `externalCoveringNumber_pos_iff`, `externalCoveringNumber_singleton`, `externalCoveringNumber_zero`, `finite_minimalCover`, `isCover_maximalSeparatedSet`, `isCover_minimalCover`, `isSeparated_maximalSeparatedSet`, `maximalSeparatedSet_subset`, `minimalCover_subset`, `packingNumber_empty`, `packingNumber_eq_zero`, `packingNumber_le_encard_self`, `packingNumber_pos_iff`, `packingNumber_singleton`, `packingNumber_two_mul_le_externalCoveringNumber`, `packingNumber_zero`	46
Total	51

Isometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coveringNumber_image` 📖	mathematical	`Isometry` `EMetricSpace.toPseudoEMetricSpace`	`Metric.coveringNumber` `Set.image` `EMetricSpace.toPseudoEMetricSpace`	—	`coveringNumber_image'` `Function.Injective.injOn` `injective`
`coveringNumber_image'` 📖	mathematical	`Isometry` `Set.InjOn`	`Metric.coveringNumber` `Set.image`	—	`le_antisymm` `LE.le.trans` `iInf_le` `iInf_congr_Prop` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.subset_preimage_image` `isCover_image_iff` `Set.encard_image_le` `Set.range_subset_iff` `Set.ext` `Set.InjOn.encard_image` `Set.InjOn.mono` `le_refl`

Metric

Definitions

Name	Category	Theorems
`coveringNumber` 📖	CompOp	18 math math: `encard_minimalCover`, `coveringNumber_two_mul_le_externalCoveringNumber`, `exists_set_encard_eq_coveringNumber`, `coveringNumber_empty`, `Isometry.coveringNumber_image'`, `coveringNumber_eq_one_of_ediam_le`, `coveringNumber_zero`, `IsCover.coveringNumber_le_encard`, `coveringNumber_pos_iff`, `Isometry.coveringNumber_image`, `coveringNumber_subset_le`, `coveringNumber_le_packingNumber`, `coveringNumber_eq_zero`, `externalCoveringNumber_le_coveringNumber`, `coveringNumber_singleton`, `coveringNumber_le_encard_self`, `coveringNumber_anti`, `coveringNumber_le_one_of_ediam_le`
`externalCoveringNumber` 📖	CompOp	14 math math: `externalCoveringNumber_eq_zero`, `coveringNumber_two_mul_le_externalCoveringNumber`, `externalCoveringNumber_le_one_of_ediam_le`, `externalCoveringNumber_empty`, `externalCoveringNumber_anti`, `packingNumber_two_mul_le_externalCoveringNumber`, `externalCoveringNumber_mono_set`, `IsCover.externalCoveringNumber_le_encard`, `externalCoveringNumber_eq_one_of_ediam_le`, `externalCoveringNumber_singleton`, `externalCoveringNumber_le_encard_self`, `externalCoveringNumber_pos_iff`, `externalCoveringNumber_le_coveringNumber`, `externalCoveringNumber_zero`
`maximalSeparatedSet` 📖	CompOp	5 math math: `maximalSeparatedSet_subset`, `isSeparated_maximalSeparatedSet`, `encard_maximalSeparatedSet`, `encard_le_of_isSeparated`, `isCover_maximalSeparatedSet`
`minimalCover` 📖	CompOp	4 math math: `encard_minimalCover`, `minimalCover_subset`, `finite_minimalCover`, `isCover_minimalCover`
`packingNumber` 📖	CompOp	11 math math: `packingNumber_eq_zero`, `packingNumber_two_mul_le_externalCoveringNumber`, `coveringNumber_le_packingNumber`, `packingNumber_singleton`, `encard_maximalSeparatedSet`, `IsSeparated.encard_le_packingNumber`, `packingNumber_zero`, `packingNumber_pos_iff`, `exists_set_encard_eq_packingNumber`, `packingNumber_empty`, `packingNumber_le_encard_self`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coveringNumber_anti` 📖	mathematical	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `NNReal.instPartialOrder`	`ENat` `instLEENat` `coveringNumber`	—	`iInf_mono` `iInf_const_mono` `IsCover.mono_radius`
`coveringNumber_empty` 📖	mathematical	—	`coveringNumber` `Set` `Set.instEmptyCollection` `ENat` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`iInf_congr_Prop` `iInf_pos` `iInf_iInf_eq_left` `Set.encard_empty`
`coveringNumber_eq_one_of_ediam_le` 📖	mathematical	`Set.Nonempty` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ediam` `ENNReal.ofNNReal`	`coveringNumber` `ENat` `AddMonoidWithOne.toOne` `instAddMonoidWithOneENat`	—	`le_antisymm` `IsCover.coveringNumber_le_encard` `IsCover.singleton_of_ediam_le` `Set.encard_singleton` `instReflLe` `NeZero.one`
`coveringNumber_eq_zero` 📖	mathematical	—	`coveringNumber` `ENat` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Set` `Set.instEmptyCollection`	—	—
`coveringNumber_le_encard_self` 📖	mathematical	—	`ENat` `instLEENat` `coveringNumber` `Set.encard`	—	`IsCover.coveringNumber_le_encard` `Set.instReflSubset`
`coveringNumber_le_one_of_ediam_le` 📖	mathematical	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ediam` `ENNReal.ofNNReal`	`ENat` `instLEENat` `coveringNumber` `AddMonoidWithOne.toOne` `instAddMonoidWithOneENat`	—	`Set.eq_empty_or_nonempty` `coveringNumber_eq_zero` `Eq.le` `coveringNumber_eq_one_of_ediam_le`
`coveringNumber_le_packingNumber` 📖	mathematical	—	`ENat` `instLEENat` `coveringNumber` `packingNumber`	—	`encard_maximalSeparatedSet` `IsCover.coveringNumber_le_encard` `maximalSeparatedSet_subset` `isCover_maximalSeparatedSet`
`coveringNumber_pos_iff` 📖	mathematical	—	`ENat` `instLTENat` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `coveringNumber` `Set.Nonempty`	—	`not_iff_not`
`coveringNumber_singleton` 📖	mathematical	—	`coveringNumber` `Set` `Set.instSingletonSet` `ENat` `AddMonoidWithOne.toOne` `instAddMonoidWithOneENat`	—	`coveringNumber_eq_one_of_ediam_le` `ediam_singleton` `ENNReal.instCanonicallyOrderedAdd`
`coveringNumber_subset_le` 📖	mathematical	`Set` `Set.instHasSubset`	`ENat` `instLEENat` `coveringNumber` `NNReal` `NNReal.instDiv` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `NNReal.instSemiring` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `coveringNumber_le_packingNumber` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Meta.NormNum.IsNNRat.to_raw_eq` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `IsStrictOrderedRing.toCharZero` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.IsNNRat.of_raw` `Mathlib.Meta.NormNum.IsNNRat.den_nz` `Mathlib.Tactic.RingNF.nat_rawCast_1` `pow_one` `mul_one` `add_zero` `packingNumber_two_mul_le_externalCoveringNumber` `externalCoveringNumber_mono_set` `externalCoveringNumber_le_coveringNumber`
`coveringNumber_two_mul_le_externalCoveringNumber` 📖	mathematical	—	`ENat` `instLEENat` `coveringNumber` `NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `NNReal.instSemiring` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat` `externalCoveringNumber`	—	`Nat.instAtLeastTwoHAddOfNat` `Set.eq_empty_or_nonempty` `coveringNumber_empty` `externalCoveringNumber_empty` `instReflLe` `LE.le.trans` `coveringNumber_le_packingNumber` `packingNumber_two_mul_le_externalCoveringNumber`
`coveringNumber_zero` 📖	mathematical	—	`coveringNumber` `EMetricSpace.toPseudoEMetricSpace` `NNReal` `NNReal.instZero` `Set.encard`	—	`le_antisymm` `coveringNumber_le_encard_self` `externalCoveringNumber_zero` `externalCoveringNumber_le_coveringNumber`
`encard_le_of_isSeparated` 📖	mathematical	`Set` `Set.instHasSubset` `IsSeparated` `ENNReal.ofNNReal`	`ENat` `instLEENat` `Set.encard` `maximalSeparatedSet`	—	`encard_maximalSeparatedSet` `le_iSup_of_le` `instReflLe`
`encard_maximalSeparatedSet` 📖	mathematical	—	`Set.encard` `maximalSeparatedSet` `packingNumber`	—	—
`encard_minimalCover` 📖	mathematical	—	`Set.encard` `minimalCover` `coveringNumber`	—	—
`exists_set_encard_eq_coveringNumber` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.Finite` `IsCover` `Set.encard` `coveringNumber`	—	`ENat.exists_eq_iInf` `Set.encard_lt_top_iff` `iInf_subtype` `iInf_congr_Prop` `iInf_and`
`exists_set_encard_eq_packingNumber` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.Finite` `IsSeparated` `ENNReal.ofNNReal` `Set.encard` `packingNumber`	—	`Set.eq_empty_or_nonempty` `iSup_congr_Prop` `iSup_iSup_eq_left` `Set.encard_empty` `iSup_pos` `ENat.exists_eq_iSup_of_lt_top` `iSup_and` `iSup_subtype` `Ne.lt_top` `Set.encard_ne_top_iff`
`externalCoveringNumber_anti` 📖	mathematical	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `NNReal.instPartialOrder`	`ENat` `instLEENat` `externalCoveringNumber`	—	`iInf_mono` `iInf_const_mono` `IsCover.mono_radius`
`externalCoveringNumber_empty` 📖	mathematical	—	`externalCoveringNumber` `Set` `Set.instEmptyCollection` `ENat` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`iInf_congr_Prop` `iInf_pos`
`externalCoveringNumber_eq_one_of_ediam_le` 📖	mathematical	`Set.Nonempty` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ediam` `ENNReal.ofNNReal`	`externalCoveringNumber` `ENat` `AddMonoidWithOne.toOne` `instAddMonoidWithOneENat`	—	`le_antisymm` `LE.le.trans_eq` `externalCoveringNumber_le_coveringNumber` `coveringNumber_eq_one_of_ediam_le` `NeZero.one`
`externalCoveringNumber_eq_zero` 📖	mathematical	—	`externalCoveringNumber` `ENat` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Set` `Set.instEmptyCollection`	—	—
`externalCoveringNumber_le_coveringNumber` 📖	mathematical	—	`ENat` `instLEENat` `externalCoveringNumber` `coveringNumber`	—	`iInf₂_le`
`externalCoveringNumber_le_encard_self` 📖	mathematical	—	`ENat` `instLEENat` `externalCoveringNumber` `Set.encard`	—	`IsCover.externalCoveringNumber_le_encard`
`externalCoveringNumber_le_one_of_ediam_le` 📖	mathematical	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ediam` `ENNReal.ofNNReal`	`ENat` `instLEENat` `externalCoveringNumber` `AddMonoidWithOne.toOne` `instAddMonoidWithOneENat`	—	`Set.eq_empty_or_nonempty` `externalCoveringNumber_eq_zero` `Eq.le` `externalCoveringNumber_eq_one_of_ediam_le`
`externalCoveringNumber_mono_set` 📖	mathematical	`Set` `Set.instHasSubset`	`ENat` `instLEENat` `externalCoveringNumber`	—	`iInf_le_of_le` `IsCover.anti` `le_rfl`
`externalCoveringNumber_pos_iff` 📖	mathematical	—	`ENat` `instLTENat` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `externalCoveringNumber` `Set.Nonempty`	—	`not_iff_not`
`externalCoveringNumber_singleton` 📖	mathematical	—	`externalCoveringNumber` `Set` `Set.instSingletonSet` `ENat` `AddMonoidWithOne.toOne` `instAddMonoidWithOneENat`	—	`externalCoveringNumber_eq_one_of_ediam_le` `ediam_singleton` `ENNReal.instCanonicallyOrderedAdd`
`externalCoveringNumber_zero` 📖	mathematical	—	`externalCoveringNumber` `EMetricSpace.toPseudoEMetricSpace` `NNReal` `NNReal.instZero` `Set.encard`	—	`le_antisymm` `externalCoveringNumber_le_encard_self` `le_iInf` `Set.encard_le_encard` `isCover_zero`
`finite_minimalCover` 📖	mathematical	—	`Set.Finite` `minimalCover`	—	—
`isCover_maximalSeparatedSet` 📖	mathematical	—	`IsCover` `maximalSeparatedSet`	—	`PseudoEMetricSpace.edist_self` `ENNReal.instCanonicallyOrderedAdd` `Mathlib.Tactic.Push.not_and_eq` `isSeparated_insert_of_notMem` `isSeparated_maximalSeparatedSet` `encard_le_of_isSeparated` `Set.encard_insert_of_notMem` `ENat.lt_add_one_iff` `encard_maximalSeparatedSet` `instReflLe`
`isCover_minimalCover` 📖	mathematical	—	`IsCover` `minimalCover`	—	—
`isSeparated_maximalSeparatedSet` 📖	mathematical	—	`IsSeparated` `ENNReal.ofNNReal` `maximalSeparatedSet`	—	—
`maximalSeparatedSet_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `maximalSeparatedSet`	—	—
`minimalCover_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `minimalCover`	—	—
`packingNumber_empty` 📖	mathematical	—	`packingNumber` `Set` `Set.instEmptyCollection` `ENat` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`iSup_congr_Prop` `iSup_iSup_eq_left` `Set.encard_empty` `iSup_pos`
`packingNumber_eq_zero` 📖	mathematical	—	`packingNumber` `ENat` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Set` `Set.instEmptyCollection`	—	—
`packingNumber_le_encard_self` 📖	mathematical	—	`ENat` `instLEENat` `packingNumber` `Set.encard`	—	`Set.encard_le_encard`
`packingNumber_pos_iff` 📖	mathematical	—	`ENat` `instLTENat` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `packingNumber` `Set.Nonempty`	—	`not_iff_not`
`packingNumber_singleton` 📖	mathematical	—	`packingNumber` `Set` `Set.instSingletonSet` `ENat` `AddMonoidWithOne.toOne` `instAddMonoidWithOneENat`	—	`le_antisymm` `LE.le.trans_eq` `packingNumber_le_encard_self` `Set.encard_singleton` `le_iSup_of_le` `Set.instReflSubset` `instReflLe`
`packingNumber_two_mul_le_externalCoveringNumber` 📖	mathematical	—	`ENat` `instLEENat` `packingNumber` `NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `NNReal.instSemiring` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat` `externalCoveringNumber`	—	`Nat.instAtLeastTwoHAddOfNat` `iSup_congr_Prop` `OrderHomClass.mono` `OrderRingHom.instOrderHomClass` `Cardinal.mk_le_of_injective` `Set.Pairwise.eq` `PseudoEMetricSpace.edist_triangle` `two_mul` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `PseudoEMetricSpace.edist_comm`
`packingNumber_zero` 📖	mathematical	—	`packingNumber` `EMetricSpace.toPseudoEMetricSpace` `NNReal` `NNReal.instZero` `Set.encard`	—	`le_antisymm` `packingNumber_le_encard_self` `le_iSup_of_le` `iSup_congr_Prop` `Set.instReflSubset` `iSup_pos` `instReflLe`

Metric.IsCover

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coveringNumber_le_encard` 📖	mathematical	`Set` `Set.instHasSubset` `Metric.IsCover`	`ENat` `instLEENat` `Metric.coveringNumber` `Set.encard`	—	`LE.le.trans` `iInf₂_le` `iInf_le`
`externalCoveringNumber_le_encard` 📖	mathematical	`Metric.IsCover`	`ENat` `instLEENat` `Metric.externalCoveringNumber` `Set.encard`	—	`iInf₂_le`

Metric.IsSeparated

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`encard_le_packingNumber` 📖	mathematical	`Set` `Set.instHasSubset` `Metric.IsSeparated` `ENNReal.ofNNReal`	`ENat` `instLEENat` `Set.encard` `Metric.packingNumber`	—	`le_iSup₂_of_le` `le_iSup_of_le` `le_rfl`

---

← Back to Index