Basic

📁 Source: Mathlib/Analysis/AperiodicOrder/Delone/Basic.lean

Statistics

Metric	Count
Definitions `DeloneSet`, `carrier`, `copy`, `coveringRadius`, `instCoeSet`, `instMembership`, `mapBilipschitz`, `mapIsometry`, `packingRadius`, `toSet`	10
Theorems `copy_eq`, `coveringRadius_pos`, `eq_of_mem_ball`, `exists_dist_le_coveringRadius`, `ext`, `ext_iff`, `isCover_coveringRadius`, `isSeparated_packingRadius`, `mapBilipschitz_carrier`, `mapBilipschitz_coveringRadius`, `mapBilipschitz_packingRadius`, `mapBilipschitz_refl`, `mapBilipschitz_trans`, `mapIsometry_apply_carrier`, `mapIsometry_apply_coveringRadius`, `mapIsometry_apply_packingRadius`, `mapIsometry_refl`, `mapIsometry_symm`, `mapIsometry_symm_apply_carrier`, `mapIsometry_symm_apply_coveringRadius`, `mapIsometry_symm_apply_packingRadius`, `mapIsometry_trans`, `mem_carrier`, `mem_coe`, `nonempty`, `packingRadius_lt_dist_of_mem_ne`, `packingRadius_pos`, `subset_ball_singleton`	28
Total	38

Delone

Definitions

Name	Category	Theorems
`DeloneSet` 📖	CompData	12 math math: `DeloneSet.mapIsometry_trans`, `DeloneSet.mem_carrier`, `DeloneSet.mem_coe`, `DeloneSet.mapIsometry_symm_apply_carrier`, `DeloneSet.mapIsometry_symm_apply_coveringRadius`, `DeloneSet.mapIsometry_symm`, `DeloneSet.mapIsometry_refl`, `DeloneSet.mapIsometry_symm_apply_packingRadius`, `DeloneSet.mapIsometry_apply_packingRadius`, `DeloneSet.mapIsometry_apply_coveringRadius`, `DeloneSet.exists_dist_le_coveringRadius`, `DeloneSet.mapIsometry_apply_carrier`

Delone.DeloneSet

Definitions

Name	Category	Theorems
`carrier` 📖	CompOp	7 math math: `isCover_coveringRadius`, `mem_carrier`, `mapIsometry_symm_apply_carrier`, `mapBilipschitz_carrier`, `isSeparated_packingRadius`, `ext_iff`, `mapIsometry_apply_carrier`
`copy` 📖	CompOp	1 math math: `copy_eq`
`coveringRadius` 📖	CompOp	7 math math: `mapBilipschitz_coveringRadius`, `isCover_coveringRadius`, `mapIsometry_symm_apply_coveringRadius`, `mapIsometry_apply_coveringRadius`, `ext_iff`, `exists_dist_le_coveringRadius`, `coveringRadius_pos`
`instCoeSet` 📖	CompOp	—
`instMembership` 📖	CompOp	3 math math: `mem_carrier`, `mem_coe`, `exists_dist_le_coveringRadius`
`mapBilipschitz` 📖	CompOp	5 math math: `mapBilipschitz_coveringRadius`, `mapBilipschitz_packingRadius`, `mapBilipschitz_carrier`, `mapBilipschitz_trans`, `mapBilipschitz_refl`
`mapIsometry` 📖	CompOp	9 math math: `mapIsometry_trans`, `mapIsometry_symm_apply_carrier`, `mapIsometry_symm_apply_coveringRadius`, `mapIsometry_symm`, `mapIsometry_refl`, `mapIsometry_symm_apply_packingRadius`, `mapIsometry_apply_packingRadius`, `mapIsometry_apply_coveringRadius`, `mapIsometry_apply_carrier`
`packingRadius` 📖	CompOp	7 math math: `mapBilipschitz_packingRadius`, `packingRadius_pos`, `mapIsometry_symm_apply_packingRadius`, `packingRadius_lt_dist_of_mem_ne`, `mapIsometry_apply_packingRadius`, `isSeparated_packingRadius`, `ext_iff`
`toSet` 📖	CompOp	2 math math: `mem_coe`, `nonempty`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`copy_eq` 📖	mathematical	`carrier` `packingRadius` `coveringRadius`	`copy`	—	`ext`
`coveringRadius_pos` 📖	mathematical	—	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal` `coveringRadius`	—	—
`eq_of_mem_ball` 📖	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `NNReal.instDiv` `packingRadius` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `Nat.instAtLeastTwoHAddOfNat` `Delone.DeloneSet` `instMembership` `Set` `Set.instMembership` `Metric.ball` `MetricSpace.toPseudoMetricSpace` `NNReal.toReal`	—	—	`Nat.instAtLeastTwoHAddOfNat` `LT.lt.not_gt` `packingRadius_lt_dist_of_mem_ne` `dist_triangle_right` `add_lt_add_of_lt_of_lt` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `add_halves` `CharZero.NeZero.two` `IsStrictOrderedRing.toCharZero` `NNReal.instIsStrictOrderedRing` `NNReal.coe_add` `add_le_add`
`exists_dist_le_coveringRadius` 📖	mathematical	—	`Delone.DeloneSet` `instMembership` `Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace` `NNReal.toReal` `coveringRadius`	—	`isCover_coveringRadius` `edist_dist`
`ext` 📖	—	`carrier` `packingRadius` `coveringRadius`	—	—	—
`ext_iff` 📖	mathematical	—	`carrier` `packingRadius` `coveringRadius`	—	`ext`
`isCover_coveringRadius` 📖	mathematical	—	`Metric.IsCover` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `coveringRadius` `Set.univ` `carrier`	—	—
`isSeparated_packingRadius` 📖	mathematical	—	`Metric.IsSeparated` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `ENNReal.ofNNReal` `packingRadius` `carrier`	—	—
`mapBilipschitz_carrier` 📖	mathematical	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal` `AntilipschitzWith` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `LipschitzWith`	`carrier` `mapBilipschitz` `Set.image`	—	—
`mapBilipschitz_coveringRadius` 📖	mathematical	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal` `AntilipschitzWith` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `LipschitzWith`	`coveringRadius` `mapBilipschitz` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	—
`mapBilipschitz_packingRadius` 📖	mathematical	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal` `AntilipschitzWith` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `LipschitzWith`	`packingRadius` `mapBilipschitz` `NNReal.instDiv`	—	—
`mapBilipschitz_refl` 📖	mathematical	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal` `instOneNNReal` `AntilipschitzWith` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.refl` `LipschitzWith`	`mapBilipschitz`	—	`ext` `Set.ext` `div_one` `Set.image_congr` `Set.image_id'` `one_mul` `NNReal.eq`
`mapBilipschitz_trans` 📖	mathematical	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal` `AntilipschitzWith` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `LipschitzWith`	`mapBilipschitz` `Equiv.trans` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `mul_pos` `NonUnitalNonAssocSemiring.toMulZeroClass` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `NNReal.instLinearOrderedCommGroupWithZero` `AntilipschitzWith.comp` `LipschitzWith.comp`	—	`ext` `mul_pos` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `AntilipschitzWith.comp` `LipschitzWith.comp` `Set.ext` `Set.image_congr` `exists_exists_and_eq_and` `NNReal.eq` `div_div` `mul_assoc`
`mapIsometry_apply_carrier` 📖	mathematical	—	`carrier` `DFunLike.coe` `Equiv` `Delone.DeloneSet` `EquivLike.toFunLike` `Equiv.instEquivLike` `mapIsometry` `Set.image` `IsometryEquiv` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `IsometryEquiv.instEquivLike`	—	—
`mapIsometry_apply_coveringRadius` 📖	mathematical	—	`coveringRadius` `DFunLike.coe` `Equiv` `Delone.DeloneSet` `EquivLike.toFunLike` `Equiv.instEquivLike` `mapIsometry`	—	—
`mapIsometry_apply_packingRadius` 📖	mathematical	—	`packingRadius` `DFunLike.coe` `Equiv` `Delone.DeloneSet` `EquivLike.toFunLike` `Equiv.instEquivLike` `mapIsometry`	—	—
`mapIsometry_refl` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Delone.DeloneSet` `EquivLike.toFunLike` `Equiv.instEquivLike` `mapIsometry` `IsometryEquiv.refl` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace`	—	`ext` `Set.ext` `Set.image_congr` `Set.image_id'` `isometry_id` `NNReal.eq`
`mapIsometry_symm` 📖	mathematical	—	`Equiv.symm` `Delone.DeloneSet` `mapIsometry` `IsometryEquiv.symm` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace`	—	—
`mapIsometry_symm_apply_carrier` 📖	mathematical	—	`carrier` `DFunLike.coe` `Equiv` `Delone.DeloneSet` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `mapIsometry` `Set.image` `IsometryEquiv` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `IsometryEquiv.instEquivLike` `IsometryEquiv.symm`	—	—
`mapIsometry_symm_apply_coveringRadius` 📖	mathematical	—	`coveringRadius` `DFunLike.coe` `Equiv` `Delone.DeloneSet` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `mapIsometry`	—	—
`mapIsometry_symm_apply_packingRadius` 📖	mathematical	—	`packingRadius` `DFunLike.coe` `Equiv` `Delone.DeloneSet` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `mapIsometry`	—	—
`mapIsometry_trans` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Delone.DeloneSet` `EquivLike.toFunLike` `Equiv.instEquivLike` `mapIsometry` `IsometryEquiv.trans` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace`	—	`ext` `Set.ext` `Set.image_congr` `NNReal.eq`
`mem_carrier` 📖	mathematical	—	`Set` `Set.instMembership` `carrier` `Delone.DeloneSet` `instMembership`	—	—
`mem_coe` 📖	mathematical	—	`Set` `Set.instMembership` `toSet` `Delone.DeloneSet` `instMembership`	—	—
`nonempty` 📖	mathematical	—	`Set.Nonempty` `toSet`	—	`Metric.IsCover.nonempty` `isCover_coveringRadius` `Set.univ_nonempty`
`packingRadius_lt_dist_of_mem_ne` 📖	mathematical	`Delone.DeloneSet` `instMembership`	`Real` `Real.instLT` `NNReal.toReal` `packingRadius` `Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace`	—	`ENNReal.ofReal_coe_nnreal` `edist_dist` `isSeparated_packingRadius` `ENNReal.ofReal_lt_ofReal_iff` `dist_pos`
`packingRadius_pos` 📖	mathematical	—	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal` `packingRadius`	—	—
`subset_ball_singleton` 📖	mathematical	—	`Real` `Real.instLT` `Real.instZero`	—	`Nat.instAtLeastTwoHAddOfNat` `half_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `packingRadius_pos` `eq_of_mem_ball` `le_rfl`

---

← Back to Index