Pointwise

📁 Source: Mathlib/Analysis/Normed/Module/Ball/Pointwise.lean

Statistics

Metric	Count
Definitions	0
Theorems `smul₀`, `Ioo_smul_sphere_zero`, `affinity_unitBall`, `affinity_unitClosedBall`, `ball_add_ball`, `ball_add_closedBall`, `ball_sub_ball`, `ball_sub_closedBall`, `closedBall_add_ball`, `closedBall_add_closedBall`, `closedBall_sub_ball`, `closedBall_sub_closedBall`, `closure_thickening`, `cthickening_ball`, `cthickening_closedBall`, `cthickening_cthickening`, `cthickening_thickening`, `diam_smul₀`, `disjoint_ball_ball_iff`, `disjoint_ball_closedBall_iff`, `disjoint_closedBall_ball_iff`, `disjoint_closedBall_closedBall_iff`, `ediam_smul_le`, `ediam_smul₀`, `eventually_singleton_add_smul_subset`, `exists_dist_eq`, `exists_dist_le_le`, `exists_dist_le_lt`, `exists_dist_lt_le`, `exists_dist_lt_lt`, `infDist_smul₀`, `infEDist_cthickening`, `infEDist_smul₀`, `infEDist_thickening`, `infEdist_cthickening`, `infEdist_smul₀`, `infEdist_thickening`, `set_smul_sphere_zero`, `smul_ball`, `smul_closedBall`, `smul_closedBall'`, `smul_sphere`, `smul_sphere'`, `smul_unitBall`, `smul_unitBall_of_pos`, `smul_unitClosedBall`, `smul_unitClosedBall_of_nonneg`, `thickening_ball`, `thickening_closedBall`, `thickening_cthickening`, `thickening_thickening`	51
Total	51

Bornology.IsBounded

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`smul₀` 📖	mathematical	`Bornology.IsBounded` `PseudoMetricSpace.toBornology` `SeminormedAddCommGroup.toPseudoMetricSpace`	`Set` `Set.smulSet` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule`	—	`LipschitzWith.isBounded_image` `lipschitzWith_smul` `NormedSpace.toIsBoundedSMul`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Ioo_smul_sphere_zero` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `Real.instLT`	`Set` `Set.smul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `Set.Ioo` `Real.instPreorder` `Metric.sphere` `SeminormedAddCommGroup.toPseudoMetricSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Set.instSDiff` `Metric.ball` `Real.instMul` `Metric.closedBall`	—	`abs_of_pos` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `LE.le.trans_lt` `set_smul_sphere_zero` `LE.le.not_gt` `Set.image_image` `Set.EqOn.image_eq` `Set.image_id` `Set.image_mul_right_Ioo` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `Set.ext` `dist_zero_right`
`affinity_unitBall` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `addGroupIsAddTorsor` `Set.smulSet` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `Metric.ball` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Real.instOne`	—	`smul_unitBall_of_pos` `vadd_ball_zero`
`affinity_unitClosedBall` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `addGroupIsAddTorsor` `Set.smulSet` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `Metric.closedBall` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Real.instOne`	—	`smul_unitClosedBall` `Real.norm_of_nonneg` `vadd_closedBall_zero`
`ball_add_ball` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Set` `Set.add` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Metric.ball` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real.instAdd`	—	`ball_add` `thickening_ball` `Metric.vadd_ball` `NormedAddGroup.to_isIsometricVAdd_left` `vadd_eq_add`
`ball_add_closedBall` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Real.instLE`	`Set` `Set.add` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Metric.ball` `SeminormedAddCommGroup.toPseudoMetricSpace` `Metric.closedBall` `Real.instAdd`	—	`ball_add` `thickening_closedBall` `Metric.vadd_ball` `NormedAddGroup.to_isIsometricVAdd_left` `vadd_eq_add`
`ball_sub_ball` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Set` `Set.sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `Metric.ball` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real.instAdd`	—	`sub_eq_add_neg` `neg_ball` `ball_add_ball`
`ball_sub_closedBall` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Real.instLE`	`Set` `Set.sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `Metric.ball` `SeminormedAddCommGroup.toPseudoMetricSpace` `Metric.closedBall` `Real.instAdd`	—	`sub_eq_add_neg` `neg_closedBall` `ball_add_closedBall`
`closedBall_add_ball` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `Real.instLT`	`Set` `Set.add` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Metric.closedBall` `SeminormedAddCommGroup.toPseudoMetricSpace` `Metric.ball` `Real.instAdd`	—	`add_comm` `ball_add_closedBall`
`closedBall_add_closedBall` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`Set` `Set.add` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Metric.closedBall` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real.instAdd`	—	`IsCompact.add_closedBall` `ProperSpace.isCompact_closedBall` `cthickening_closedBall` `Metric.vadd_closedBall` `NormedAddGroup.to_isIsometricVAdd_left` `vadd_eq_add` `add_comm`
`closedBall_sub_ball` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `Real.instLT`	`Set` `Set.sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `Metric.closedBall` `SeminormedAddCommGroup.toPseudoMetricSpace` `Metric.ball` `Real.instAdd`	—	`sub_eq_add_neg` `neg_ball` `closedBall_add_ball`
`closedBall_sub_closedBall` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`Set` `Set.sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `Metric.closedBall` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real.instAdd`	—	`sub_eq_add_neg` `neg_closedBall` `closedBall_add_closedBall`
`closure_thickening` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`closure` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Metric.thickening` `PseudoMetricSpace.toPseudoEMetricSpace` `Metric.cthickening`	—	`Metric.cthickening_zero` `cthickening_thickening` `le_rfl` `zero_add`
`cthickening_ball` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `Real.instLT`	`Metric.cthickening` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Metric.ball` `Metric.closedBall` `Real.instAdd`	—	`Metric.thickening_singleton` `cthickening_thickening` `Metric.cthickening_singleton` `add_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `LT.lt.le`
`cthickening_closedBall` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`Metric.cthickening` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Metric.closedBall` `Real.instAdd`	—	`Metric.cthickening_singleton` `cthickening_cthickening` `add_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid`
`cthickening_cthickening` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`Metric.cthickening` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real.instAdd`	—	`HasSubset.Subset.antisymm` `Set.instAntisymmSubset` `Metric.cthickening_cthickening_subset` `ENNReal.ofReal_add` `infEDist_cthickening` `tsub_le_iff_right` `ENNReal.instOrderedSub`
`cthickening_thickening` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `Real.instLT`	`Metric.cthickening` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Metric.thickening` `Real.instAdd`	—	`HasSubset.Subset.antisymm` `Set.instAntisymmSubset` `Metric.cthickening_thickening_subset` `ENNReal.ofReal_add` `LT.lt.le` `infEDist_thickening` `tsub_le_iff_right` `ENNReal.instOrderedSub`
`diam_smul₀` 📖	mathematical	—	`Metric.diam` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set` `Set.smulSet` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Real` `Real.instMul` `Norm.norm` `NormedDivisionRing.toNorm`	—	`ediam_smul₀` `ENNReal.toReal_smul`
`disjoint_ball_ball_iff` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Metric.ball` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real.instLE` `Real.instAdd` `Dist.dist` `PseudoMetricSpace.toDist`	—	`le_of_not_gt` `exists_dist_lt_lt` `add_comm` `Disjoint.le_bot` `dist_comm` `Metric.ball_disjoint_ball`
`disjoint_ball_closedBall_iff` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Real.instLE`	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Metric.ball` `SeminormedAddCommGroup.toPseudoMetricSpace` `Metric.closedBall` `Real.instAdd` `Dist.dist` `PseudoMetricSpace.toDist`	—	`le_of_not_gt` `exists_dist_lt_le` `add_comm` `Disjoint.le_bot` `dist_comm` `Metric.ball_disjoint_closedBall`
`disjoint_closedBall_ball_iff` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `Real.instLT`	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Metric.closedBall` `SeminormedAddCommGroup.toPseudoMetricSpace` `Metric.ball` `Real.instAdd` `Dist.dist` `PseudoMetricSpace.toDist`	—	`disjoint_comm` `disjoint_ball_closedBall_iff` `add_comm` `dist_comm`
`disjoint_closedBall_closedBall_iff` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Metric.closedBall` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real.instLT` `Real.instAdd` `Dist.dist` `PseudoMetricSpace.toDist`	—	`lt_of_not_ge` `exists_dist_le_le` `add_comm` `Disjoint.le_bot` `dist_comm` `Metric.closedBall_disjoint_closedBall`
`ediam_smul_le` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Metric.ediam` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set` `Set.smulSet` `SMulZeroClass.toSMul` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NNReal` `Algebra.toSMul` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`LipschitzWith.ediam_image_le` `lipschitzWith_smul`
`ediam_smul₀` 📖	mathematical	—	`Metric.ediam` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set` `Set.smulSet` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NNReal` `ENNReal` `Algebra.toSMul` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `NormedDivisionRing.toNormedRing`	—	`le_antisymm` `ediam_smul_le` `NormSMulClass.toIsBoundedSMul` `eq_or_ne` `Set.eq_empty_or_nonempty` `nnnorm_zero` `Metric.ediam_empty` `smul_zero` `Set.smul_set_empty` `zero_smul` `Set.zero_smul_set` `Metric.ediam_singleton` `LipschitzWith.ediam_image_le` `lipschitzWith_smul` `le_inv_smul_iff_of_pos` `PosSMulStrictMono.toPosSMulMono` `ENNReal.instPosSMulStrictMonoNNReal` `PosSMulMono.toPosSMulReflectLE` `NNReal.instIsStrictOrderedRing` `nnnorm_pos` `nnnorm_inv` `inv_smul_smul₀` `Set.image_smul` `ENNReal.smul_def` `smul_eq_mul`
`eventually_singleton_add_smul_subset` 📖	mathematical	`Bornology.IsBounded` `PseudoMetricSpace.toBornology` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set` `Filter` `Filter.instMembership` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace`	`Filter.Eventually` `Set.instHasSubset` `Set.add` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Set.instSingletonSet` `Set.smulSet` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `NormedSpace.toModule` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing`	—	`Filter.HasBasis.mem_iff` `Metric.nhds_basis_closedBall` `Bornology.IsBounded.subset_closedBall_lt` `Metric.closedBall_mem_nhds` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Filter.mp_mem` `Filter.univ_mem'` `Set.singleton_add` `Set.image_add_left` `norm_smul` `NormedSpace.toNormSMulClass` `mul_le_mul` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `IsOrderedRing.toMulPosMono` `mem_closedBall_zero_iff` `norm_nonneg` `le_of_lt` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `div_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `mul_one` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `one_mul` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `ne_of_gt` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `add_neg_cancel_left` `dist_eq_norm` `add_sub_cancel_left`
`exists_dist_eq` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `Real.instAdd` `Real.instOne`	`Dist.dist` `PseudoMetricSpace.toDist` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real.instMul`	—	`one_smul` `add_smul` `dist_eq_norm` `add_sub_add_left_eq_sub` `norm_smul_of_nonneg` `add_sub_add_right_eq_sub`
`exists_dist_le_le` 📖	—	`Real` `Real.instLE` `Real.instZero` `Dist.dist` `PseudoMetricSpace.toDist` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real.instAdd`	—	—	`LE.le.eq_or_lt` `zero_add` `Eq.le` `dist_self` `add_pos_of_pos_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `div_mul_comm` `mul_le_of_le_one_left` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `div_le_one` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `exists_dist_eq` `div_nonneg` `add_nonneg` `add_div` `div_self` `LT.lt.ne'`
`exists_dist_le_lt` 📖	—	`Real` `Real.instLE` `Real.instZero` `Real.instLT` `Dist.dist` `PseudoMetricSpace.toDist` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real.instAdd`	—	—	`div_mul_comm` `mul_le_of_le_one_left` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `LT.lt.le` `div_lt_one` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `add_pos_of_pos_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `mul_lt_of_lt_one_left` `IsStrictOrderedRing.toMulPosStrictMono` `exists_dist_eq` `div_nonneg` `add_nonneg` `add_div` `div_self` `LT.lt.ne'`
`exists_dist_lt_le` 📖	—	`Real` `Real.instLT` `Real.instZero` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real.instAdd`	—	—	`exists_dist_le_lt` `dist_comm` `add_comm`
`exists_dist_lt_lt` 📖	—	`Real` `Real.instLT` `Real.instZero` `Dist.dist` `PseudoMetricSpace.toDist` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real.instAdd`	—	—	`div_mul_comm` `mul_lt_of_lt_one_left` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `div_lt_one` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `add_pos` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `exists_dist_eq` `div_nonneg` `LT.lt.le` `add_nonneg` `add_div` `div_self` `LT.lt.ne'`
`infDist_smul₀` 📖	mathematical	—	`Metric.infDist` `SeminormedAddCommGroup.toPseudoMetricSpace` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Set` `Set.smulSet` `Real` `Real.instMul` `Norm.norm` `NormedDivisionRing.toNorm`	—	`infEDist_smul₀` `ENNReal.toReal_smul`
`infEDist_cthickening` 📖	mathematical	—	`Metric.infEDist` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Metric.cthickening` `ENNReal` `ENNReal.instSub` `ENNReal.ofReal`	—	`le_or_gt` `Metric.cthickening_of_nonpos` `Metric.infEDist_closure` `ENNReal.ofReal_of_nonpos` `tsub_zero` `ENNReal.instOrderedSub` `closure_thickening` `infEDist_thickening`
`infEDist_smul₀` 📖	mathematical	—	`Metric.infEDist` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Set` `Set.smulSet` `NNReal` `ENNReal` `Algebra.toSMul` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `NormedDivisionRing.toNormedRing`	—	`smul_inv_smul₀` `Function.Surjective.iInf_congr` `iInf_congr_Prop` `Set.smul_mem_smul_set_iff₀` `edist_smul₀` `ENNReal.mul_iInf_of_ne` `ENNReal.coe_ne_top`
`infEDist_thickening` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Metric.infEDist` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Metric.thickening` `ENNReal` `ENNReal.instSub` `ENNReal.ofReal`	—	`lt_or_ge` `Metric.infEDist_zero_of_mem` `tsub_eq_zero_of_le` `ENNReal.instCanonicallyOrderedAdd` `ENNReal.instOrderedSub` `LT.lt.le` `LE.le.antisymm'` `tsub_le_iff_right` `Metric.infEDist_le_infEDist_thickening_add` `ENNReal.le_sub_of_add_le_right` `ENNReal.ofReal_ne_top` `Metric.le_infEDist` `le_of_forall_gt` `ENNReal.add_lt_top` `lt_top_iff_ne_top` `Metric.infEDist_ne_top` `Metric.self_subset_thickening` `ENNReal.ofReal_lt_top` `sub_pos_of_lt` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `LE.le.trans_lt` `Metric.infEDist_le_edist_of_mem` `ENNReal.ofReal_eq_coe_nnreal` `exists_dist_lt_lt` `add_sub_cancel` `dist_lt_coe` `edist_lt_coe` `LT.lt.trans_le` `ENNReal.add_lt_add_right` `Metric.infEDist_lt_iff` `Metric.mem_thickening_iff` `edist_lt_ofReal` `ENNReal.ofReal_add` `sub_add_cancel` `ENNReal.ofReal_coe_nnreal` `le_refl`
`infEdist_cthickening` 📖	mathematical	—	`Metric.infEDist` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Metric.cthickening` `ENNReal` `ENNReal.instSub` `ENNReal.ofReal`	—	`infEDist_cthickening`
`infEdist_smul₀` 📖	mathematical	—	`Metric.infEDist` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Set` `Set.smulSet` `NNReal` `ENNReal` `Algebra.toSMul` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `NormedDivisionRing.toNormedRing`	—	`infEDist_smul₀`
`infEdist_thickening` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Metric.infEDist` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Metric.thickening` `ENNReal` `ENNReal.instSub` `ENNReal.ofReal`	—	`infEDist_thickening`
`set_smul_sphere_zero` 📖	mathematical	`Set` `Set.instMembership` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing`	`Set.smul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Metric.sphere` `SeminormedAddCommGroup.toPseudoMetricSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Set.preimage` `Real` `Norm.norm` `SeminormedAddCommGroup.toNorm` `Set.image` `Real.instMul` `NormedField.toNorm`	—	`Set.iUnion_smul_left_image` `Set.iUnion₂_congr` `smul_sphere'` `smul_zero` `Set.ext` `sub_zero`
`smul_ball` 📖	mathematical	—	`Set` `Set.smulSet` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Metric.ball` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real` `Real.instMul` `Norm.norm` `NormedField.toNorm`	—	`Set.ext` `Set.mem_smul_set_iff_inv_smul_mem₀` `inv_smul_smul₀` `dist_smul₀` `NormedSpace.toNormSMulClass` `norm_inv` `div_lt_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `norm_pos_iff` `mul_comm`
`smul_closedBall` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`Set` `Set.smulSet` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Metric.closedBall` `Real.instMul` `Norm.norm` `NormedField.toNorm`	—	`eq_or_ne` `Set.zero_smul_set` `zero_smul` `norm_zero` `MulZeroClass.zero_mul` `Metric.closedBall_zero` `smul_closedBall'`
`smul_closedBall'` 📖	mathematical	—	`Set` `Set.smulSet` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Metric.closedBall` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real` `Real.instMul` `Norm.norm` `NormedField.toNorm`	—	`Set.smul_set_union` `smul_ball` `smul_sphere'`
`smul_sphere` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`Set` `Set.smulSet` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Metric.sphere` `Real.instMul` `Norm.norm` `NormedField.toNorm`	—	`eq_or_ne` `Set.zero_smul_set` `EMetric.instNontrivialTopologyOfNontrivial` `zero_smul` `norm_zero` `MulZeroClass.zero_mul` `Metric.sphere_zero` `smul_sphere'`
`smul_sphere'` 📖	mathematical	—	`Set` `Set.smulSet` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Metric.sphere` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real` `Real.instMul` `Norm.norm` `NormedField.toNorm`	—	`Set.ext` `Set.mem_smul_set_iff_inv_smul_mem₀` `inv_smul_smul₀` `dist_smul₀` `NormedSpace.toNormSMulClass` `norm_inv` `div_eq_iff` `LT.lt.ne'` `norm_pos_iff` `mul_comm`
`smul_unitBall` 📖	mathematical	—	`Set` `Set.smulSet` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Metric.ball` `SeminormedAddCommGroup.toPseudoMetricSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Real` `Real.instOne` `Norm.norm` `NormedField.toNorm`	—	`smul_ball` `smul_zero` `mul_one`
`smul_unitBall_of_pos` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Set` `Set.smulSet` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `Metric.ball` `SeminormedAddCommGroup.toPseudoMetricSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Real.instOne`	—	`smul_unitBall` `LT.lt.ne'` `Real.norm_of_nonneg` `LT.lt.le`
`smul_unitClosedBall` 📖	mathematical	—	`Set` `Set.smulSet` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Metric.closedBall` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Real` `Real.instOne` `Norm.norm` `NormedField.toNorm`	—	`smul_closedBall` `zero_le_one` `Real.instZeroLEOneClass` `smul_zero` `mul_one`
`smul_unitClosedBall_of_nonneg` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`Set` `Set.smulSet` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `Metric.closedBall` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Real.instOne`	—	`smul_unitClosedBall` `Real.norm_of_nonneg`
`thickening_ball` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Metric.thickening` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Metric.ball` `Real.instAdd`	—	`Metric.thickening_singleton` `thickening_thickening`
`thickening_closedBall` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Real.instLE`	`Metric.thickening` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Metric.closedBall` `Metric.ball` `Real.instAdd`	—	`Metric.cthickening_singleton` `thickening_cthickening` `Metric.thickening_singleton`
`thickening_cthickening` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Real.instLE`	`Metric.thickening` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Metric.cthickening` `Real.instAdd`	—	`LE.le.eq_or_lt` `Metric.cthickening_zero` `Metric.thickening_closure` `add_zero` `closure_thickening` `thickening_thickening`
`thickening_thickening` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Metric.thickening` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real.instAdd`	—	`HasSubset.Subset.antisymm` `Set.instAntisymmSubset` `Metric.thickening_thickening_subset` `exists_dist_lt_lt` `add_comm`

---

← Back to Index