Documentation Verification Report

Real

📁 Source: Mathlib/Analysis/Normed/Module/RCLike/Real.lean

Statistics

Metric	Count
Definitions	0
Theorems `sphere_nonempty`, `punctured_nhds_module_neBot`, `closure_ball`, `dist_smul_add_one_sub_smul_le`, `exists_norm_eq`, `frontier_ball`, `frontier_closedBall`, `frontier_closedBall'`, `frontier_sphere`, `frontier_sphere'`, `interior_closedBall`, `interior_closedBall'`, `interior_sphere`, `interior_sphere'`, `inv_norm_smul_mem_unitClosedBall`, `nnnorm_surjective`, `norm_smul_of_nonneg`, `range_nnnorm`, `range_norm`	19
Total	19

NormedSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sphere_nonempty` 📖	mathematical	—	`Set.Nonempty` `Metric.sphere` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real` `Real.instLE` `Real.instZero`	—	`Metric.nonempty_closedBall` `Set.Nonempty.mono` `Metric.sphere_subset_closedBall` `exists_norm_eq` `add_sub_cancel_left`

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`punctured_nhds_module_neBot` 📖	mathematical	—	`Filter.NeBot` `nhdsWithin` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet`	—	`Module.punctured_nhds_neBot` `instIsDomain` `NormedField.nhdsNE_neBot` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_ball` 📖	mathematical	—	`closure` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Metric.ball` `Metric.closedBall`	—	`Set.Subset.antisymm` `Metric.closure_ball_subset_closedBall` `ContinuousWithinAt.fun_add` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousAt.continuousWithinAt` `ContinuousAt.smul` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `continuousAt_id'` `continuousAt_const` `continuousWithinAt_const` `one_smul` `sub_add_cancel` `ContinuousWithinAt.mem_closure` `closure_Ico` `zero_ne_one` `instOrderTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Real.instZeroLEOneClass` `Metric.mem_ball` `dist_eq_norm` `add_sub_cancel_right` `norm_smul` `NormedSpace.toNormSMulClass` `Real.norm_eq_abs` `abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `mul_comm` `mul_one` `LE.le.lt_of_ne` `LE.le.trans` `norm_nonneg` `Metric.mem_closedBall` `mul_lt_mul'` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing`
`dist_smul_add_one_sub_smul_le` 📖	mathematical	`Real` `Set` `Set.instMembership` `Set.Icc` `Real.instPreorder` `Real.instZero` `Real.instOne`	`Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `SeminormedAddCommGroup.toPseudoMetricSpace` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `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` `NormedSpace.toModule` `Real.normedField` `Real.instSub`	—	`dist_eq_norm'` `NormedSpace.toNormSMulClass` `sub_smul` `one_smul` `smul_sub` `sub_right_comm` `Real.norm_eq_abs` `abs_eq_self` `Real.instIsOrderedAddMonoid` `sub_nonneg` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `sub_le_sub_left` `dist_nonneg` `sub_zero` `one_mul`
`exists_norm_eq` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`Norm.norm` `SeminormedAddCommGroup.toNorm`	—	`exists_norm_ne_zero` `norm_smul` `NormedSpace.toNormSMulClass` `Real.norm_of_nonneg` `norm_inv` `norm_norm` `inv_mul_cancel₀` `mul_one`
`frontier_ball` 📖	mathematical	—	`frontier` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Metric.ball` `Metric.sphere`	—	`frontier.eq_1` `closure_ball` `IsOpen.interior_eq` `Metric.isOpen_ball` `Metric.closedBall_diff_ball`
`frontier_closedBall` 📖	mathematical	—	`frontier` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Metric.closedBall` `Metric.sphere`	—	`frontier.eq_1` `Metric.closure_closedBall` `interior_closedBall` `Metric.closedBall_diff_ball`
`frontier_closedBall'` 📖	mathematical	—	`frontier` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Metric.closedBall` `Metric.sphere`	—	`frontier.eq_1` `Metric.closure_closedBall` `interior_closedBall'` `Metric.closedBall_diff_ball`
`frontier_sphere` 📖	mathematical	—	`frontier` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Metric.sphere`	—	`IsClosed.frontier_eq` `Metric.isClosed_sphere` `interior_sphere` `Set.diff_empty`
`frontier_sphere'` 📖	mathematical	—	`frontier` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Metric.sphere`	—	`IsClosed.frontier_eq` `Metric.isClosed_sphere` `interior_sphere'` `Set.diff_empty`
`interior_closedBall` 📖	mathematical	—	`interior` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Metric.closedBall` `Metric.ball`	—	`Ne.lt_or_gt` `Metric.closedBall_eq_empty` `Metric.ball_eq_empty` `LT.lt.le` `interior_empty` `Set.Subset.antisymm` `LE.le.lt_or_eq` `Metric.mem_closedBall` `interior_subset` `Set.mem_Icc` `abs_le` `Real.instIsOrderedAddMonoid` `Real.norm_eq_abs` `mul_le_mul_iff_left₀` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `dist_eq_norm` `one_mul` `add_sub_cancel_right` `norm_smul` `NormedSpace.toNormSMulClass` `interior_mono` `preimage_interior_subset_interior_preimage` `Continuous.fun_add` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Continuous.smul` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `continuous_id'` `continuous_const` `one_smul` `sub_add_cancel` `interior_Icc` `instOrderTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `instNoMinOrderOfNontrivial` `Real.instNontrivial` `instNoMaxOrderOfNontrivial` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Metric.ball_subset_interior_closedBall`
`interior_closedBall'` 📖	mathematical	—	`interior` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Metric.closedBall` `Metric.ball`	—	`eq_or_ne` `Metric.closedBall_zero` `Metric.ball_zero` `interior_singleton` `Real.punctured_nhds_module_neBot` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `interior_closedBall`
`interior_sphere` 📖	mathematical	—	`interior` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Metric.sphere` `Set` `Set.instEmptyCollection`	—	`frontier_closedBall` `interior_frontier` `Metric.isClosed_closedBall`
`interior_sphere'` 📖	mathematical	—	`interior` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Metric.sphere` `Set` `Set.instEmptyCollection`	—	`frontier_closedBall'` `interior_frontier` `Metric.isClosed_closedBall`
`inv_norm_smul_mem_unitClosedBall` 📖	mathematical	—	`Set` `Set.instMembership` `Metric.closedBall` `SeminormedAddCommGroup.toPseudoMetricSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Real` `Real.instOne` `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` `NormedSpace.toModule` `Real.normedField` `Real.instInv` `Norm.norm` `SeminormedAddCommGroup.toNorm`	—	`norm_smul` `NormedSpace.toNormSMulClass` `norm_inv` `norm_norm` `Real.instZeroLEOneClass`
`nnnorm_surjective` 📖	mathematical	—	`NNReal` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`NNReal.eq` `exists_norm_eq` `NNReal.coe_nonneg`
`norm_smul_of_nonneg` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`Norm.norm` `SeminormedAddCommGroup.toNorm` `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` `Real.instMul`	—	`norm_smul` `NormedSpace.toNormSMulClass` `Real.norm_eq_abs` `abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid`
`range_nnnorm` 📖	mathematical	—	`Set.range` `NNReal` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Set.univ`	—	`Function.Surjective.range_eq` `nnnorm_surjective`
`range_norm` 📖	mathematical	—	`Set.range` `Real` `Norm.norm` `SeminormedAddCommGroup.toNorm` `Set.Ici` `Real.instPreorder` `Real.instZero`	—	`Set.Subset.antisymm` `Set.range_subset_iff` `norm_nonneg` `exists_norm_eq`

---

← Back to Index