Documentation Verification Report

Schwarz

📁 Source: Mathlib/Analysis/Complex/Schwarz.lean

Statistics

Metric	Count
Definitions	0
Theorems `affine_of_mapsTo_ball_of_exists_norm_dslope_eq_div`, `affine_of_mapsTo_ball_of_exists_norm_dslope_eq_div'`, `affine_of_mapsTo_ball_of_norm_dslope_eq_div`, `dist_le_dist_of_mapsTo_ball`, `dist_le_dist_of_mapsTo_ball_self`, `dist_le_div_mul_dist_of_mapsTo_ball`, `dist_le_mul_div_pow_of_mapsTo_ball_of_isLittleO`, `norm_deriv_le_div_of_mapsTo_ball`, `norm_deriv_le_one_of_mapsTo_ball`, `norm_dslope_le_div_of_mapsTo_ball`, `norm_fderiv_le_div_of_mapsTo_ball`, `norm_fderiv_le_one_of_mapsTo_ball`, `norm_le_norm_of_mapsTo_ball`, `norm_le_norm_of_mapsTo_ball_self`	14
Total	14

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`affine_of_mapsTo_ball_of_exists_norm_dslope_eq_div` 📖	mathematical	`DifferentiableOn` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `addCommGroup` `instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddCommGroup.toPseudoMetricSpace` `Metric.ball` `Set.MapsTo` `Metric.closedBall` `Set` `Set.instMembership` `Norm.norm` `NormedAddCommGroup.toNorm` `dslope` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid`	`Set.EqOn` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `Module.toDistribMulAction` `instSub`	—	`affine_of_mapsTo_ball_of_norm_dslope_eq_div`
`affine_of_mapsTo_ball_of_exists_norm_dslope_eq_div'` 📖	mathematical	`DifferentiableOn` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `addCommGroup` `instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddCommGroup.toPseudoMetricSpace` `Metric.ball` `Set.MapsTo` `Metric.closedBall` `Set` `Set.instMembership` `Norm.norm` `NormedAddCommGroup.toNorm` `dslope` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid`	`Set.EqOn` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `Module.toDistribMulAction` `instSub`	—	`affine_of_mapsTo_ball_of_norm_dslope_eq_div`
`affine_of_mapsTo_ball_of_norm_dslope_eq_div` 📖	mathematical	`DifferentiableOn` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `addCommGroup` `instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddCommGroup.toPseudoMetricSpace` `Metric.ball` `Set.MapsTo` `Metric.closedBall` `Set` `Set.instMembership` `Norm.norm` `NormedAddCommGroup.toNorm` `dslope` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid`	`Set.EqOn` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `Module.toDistribMulAction` `instSub`	—	`SeminormedAddCommGroup.to_isUniformAddGroup` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `Metric.nonempty_ball` `ContinuousLinearMap.dslope_comp` `DifferentiableOn.differentiableAt` `Metric.ball_mem_nhds` `norm_dslope_le_div_of_mapsTo_ball` `Differentiable.comp_differentiableOn` `ContinuousLinearMap.differentiable` `UniformSpace.Completion.dist_eq` `isMaxOn_iff` `UniformSpace.Completion.norm_coe` `differentiableOn_dslope` `UniformSpace.Completion.completeSpace` `IsOpen.mem_nhds` `Metric.isOpen_ball` `Metric.mem_ball_self` `norm_eqOn_of_isPreconnected_of_isMaxOn` `Convex.isPreconnected` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `IsBoundedSMul.continuousSMul` `convex_ball` `DifferentiableOn.add_const` `IsMaxOn.norm_add_self` `eq_of_norm_eq_of_norm_add_eq` `SameRay.norm_add` `SameRay.rfl` `Real.instIsStrictOrderedRing` `sub_smul_dslope` `add_sub_cancel`
`dist_le_dist_of_mapsTo_ball` 📖	mathematical	`DifferentiableOn` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `instNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Metric.ball` `Set.MapsTo` `Metric.closedBall` `Set` `Set.instMembership`	`Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist`	—	`div_self` `LT.lt.ne'` `Metric.nonempty_ball` `one_mul` `dist_le_div_mul_dist_of_mapsTo_ball`
`dist_le_dist_of_mapsTo_ball_self` 📖	mathematical	`DifferentiableOn` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `instNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Metric.ball` `Set.MapsTo` `Metric.closedBall` `Set` `Set.instMembership`	`Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist`	—	`dist_le_dist_of_mapsTo_ball`
`dist_le_div_mul_dist_of_mapsTo_ball` 📖	mathematical	`DifferentiableOn` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `instNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Metric.ball` `Set.MapsTo` `Metric.closedBall` `Set` `Set.instMembership`	`Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `Real.instMul` `DivInvMonoid.toDiv` `Real.instDivInvMonoid`	—	`LE.le.trans_eq` `dist_le_mul_div_pow_of_mapsTo_ball_of_isLittleO` `pow_zero` `NormedDivisionRing.to_normOneClass` `sub_self` `Filter.Tendsto.sub_const` `IsTopologicalAddGroup.to_continuousSub` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousOn.continuousAt` `DifferentiableOn.continuousOn` `IsTopologicalAddGroup.toContinuousAdd` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Metric.ball_mem_nhds` `Metric.nonempty_ball` `zero_add` `pow_one` `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.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_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` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div'` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial`
`dist_le_mul_div_pow_of_mapsTo_ball_of_isLittleO` 📖	mathematical	`DifferentiableOn` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `instNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Metric.ball` `Set.MapsTo` `Metric.closedBall` `Asymptotics.IsLittleO` `Real` `NormedAddCommGroup.toNorm` `Real.norm` `nhds` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Monoid.toNatPow` `Real.instMonoid` `Norm.norm` `Set` `Set.instMembership`	`Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `Real.instMul` `DivInvMonoid.toDiv` `Real.instDivInvMonoid`	—	`Metric.nonempty_ball` `Metric.nonempty_closedBall` `eq_or_ne` `dist_self` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `pow_nonneg` `IsOrderedRing.toZeroLEOneClass` `Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `dist_nonneg` `exists_dual_vector` `Iff.not` `norm_sub_eq_zero_iff` `dist_lineMap_left` `dist_comm` `dist_zero_right` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Set.MapsTo.comp` `AffineMap.lineMap_apply_zero` `RingHomIsometric.ids` `one_mul` `LipschitzWith.mapsTo_closedBall` `ContinuousLinearMap.lipschitz` `Differentiable.comp_differentiableOn` `ContinuousLinearMap.differentiable` `DifferentiableOn.comp` `AffineMap.differentiableOn` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `sub_zero` `Asymptotics.IsBigO.trans_isLittleO` `ContinuousLinearMap.isBigO_comp` `Asymptotics.IsLittleO.trans_isBigO` `Asymptotics.IsLittleO.comp_tendsto` `Continuous.tendsto` `Continuous.comp'` `AffineMap.lineMap_continuous_uncurry` `instIsTopologicalAddTorsor_1` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Continuous.prodMk` `continuous_const` `continuous_id'` `mul_comm` `mul_pow` `norm_pow` `NormedDivisionRing.to_normOneClass` `NormedDivisionRing.toNormMulClass` `Asymptotics.IsBigO.const_mul_left` `Asymptotics.IsBigO.norm_left` `Asymptotics.isBigO_refl` `CStarRing.norm_of_mem_unitary` `RCLike.instCStarRing` `instNontrivial` `SubmonoidClass.toOneMemClass` `Submonoid.instSubmonoidClass` `dist_eq_norm_sub` `AffineMap.lineMap_apply_one` `map_sub` `norm_real` `norm_norm` `one_div` `inv_div`
`norm_deriv_le_div_of_mapsTo_ball` 📖	mathematical	`DifferentiableOn` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `addCommGroup` `instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddCommGroup.toPseudoMetricSpace` `Metric.ball` `Set.MapsTo` `Metric.closedBall` `Real` `Real.instLT` `Real.instZero`	`Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `deriv` `DivInvMonoid.toDiv` `Real.instDivInvMonoid`	—	`norm_deriv_eq_norm_fderiv` `norm_fderiv_le_div_of_mapsTo_ball`
`norm_deriv_le_one_of_mapsTo_ball` 📖	mathematical	`DifferentiableOn` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `addCommGroup` `instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddCommGroup.toPseudoMetricSpace` `Metric.ball` `Set.MapsTo` `Metric.closedBall` `Real` `Real.instLT` `Real.instZero`	`Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `deriv` `Real.instOne`	—	`LE.le.trans_eq` `norm_deriv_le_div_of_mapsTo_ball` `div_self` `LT.lt.ne'`
`norm_dslope_le_div_of_mapsTo_ball` 📖	mathematical	`DifferentiableOn` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `addCommGroup` `instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddCommGroup.toPseudoMetricSpace` `Metric.ball` `Set.MapsTo` `Metric.closedBall` `Set` `Set.instMembership`	`Real` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `dslope` `DivInvMonoid.toDiv` `Real.instDivInvMonoid`	—	`eq_or_ne` `dslope_same` `norm_deriv_le_div_of_mapsTo_ball` `dist_self` `dslope_of_ne` `slope_def_module` `norm_smul` `NormedSpace.toNormSMulClass` `norm_inv` `dist_eq_norm_sub` `div_eq_inv_mul` `div_le_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `dist_le_div_mul_dist_of_mapsTo_ball`
`norm_fderiv_le_div_of_mapsTo_ball` 📖	mathematical	`DifferentiableOn` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `instNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Metric.ball` `Set.MapsTo` `Metric.closedBall` `Real` `Real.instLT` `Real.instZero`	`Real.instLE` `Norm.norm` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.hasOpNorm` `fderiv` `DivInvMonoid.toDiv` `Real.instDivInvMonoid`	—	`Metric.nonempty_closedBall` `Set.MapsTo.nonempty` `Metric.nonempty_ball` `norm_fderiv_le_of_lip'` `Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Filter.mp_mem` `Metric.ball_mem_nhds` `Filter.univ_mem'` `dist_eq_norm_sub` `dist_le_div_mul_dist_of_mapsTo_ball`
`norm_fderiv_le_one_of_mapsTo_ball` 📖	mathematical	`DifferentiableOn` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `instNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Metric.ball` `Set.MapsTo` `Metric.closedBall` `Real` `Real.instLT` `Real.instZero`	`Real.instLE` `Norm.norm` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.hasOpNorm` `fderiv` `Real.instOne`	—	`div_self` `LT.lt.ne'` `norm_fderiv_le_div_of_mapsTo_ball`
`norm_le_norm_of_mapsTo_ball` 📖	mathematical	`DifferentiableOn` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `instNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Metric.ball` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Set.MapsTo` `Metric.closedBall` `Real` `Real.instLT` `Norm.norm` `NormedAddCommGroup.toNorm`	`Real.instLE`	—	`dist_zero_right` `dist_le_dist_of_mapsTo_ball` `mem_ball_zero_iff`
`norm_le_norm_of_mapsTo_ball_self` 📖	mathematical	`DifferentiableOn` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `instNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Metric.ball` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Set.MapsTo` `Metric.closedBall` `Real` `Real.instLT` `Norm.norm` `NormedAddCommGroup.toNorm`	`Real.instLE`	—	`norm_le_norm_of_mapsTo_ball`

---

← Back to Index