Documentation Verification Report

Ray

📁 Source: Mathlib/Analysis/Normed/Module/Ray.lean

Statistics

Metric	Count
Definitions `Ray`	1
Theorems `eq_of_norm_eq`, `inv_norm_smul_eq`, `norm_add`, `norm_eq_iff`, `norm_smul_eq`, `norm_sub`, `norm_injOn_ray_left`, `norm_injOn_ray_right`, `not_sameRay_iff_of_norm_eq`, `sameRay_iff_inv_norm_smul_eq`, `sameRay_iff_inv_norm_smul_eq_of_ne`, `sameRay_iff_norm_smul_eq`, `sameRay_iff_of_norm_eq`	13
Total	14

Module

Definitions

Name	Category	Theorems
`Ray` 📖	CompOp	14 math math: `units_inv_smul`, `Ray.neg_units_smul`, `Ray.units_smul_of_neg`, `smul_rayOfNeZero`, `Ray.map_symm`, `Ray.linearEquiv_smul_eq_map`, `units_smul_eq_self_iff`, `units_smul_eq_neg_iff`, `Ray.map_refl`, `Ray.units_smul_of_pos`, `neg_rayOfNeZero`, `instNonemptyRayOfNontrivial`, `Ray.map_apply`, `Ray.map_neg`

SameRay

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_of_norm_eq` 📖	—	`SameRay` `Real` `Real.instCommSemiring` `Real.partialOrder` `Real.instIsStrictOrderedRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `Norm.norm` `NormedAddCommGroup.toNorm`	—	—	`Real.instIsStrictOrderedRing` `sameRay_iff_of_norm_eq`
`inv_norm_smul_eq` 📖	mathematical	`SameRay` `Real` `Real.instCommSemiring` `Real.partialOrder` `Real.instIsStrictOrderedRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `Real.instInv` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`Real.instIsStrictOrderedRing` `sameRay_iff_inv_norm_smul_eq_of_ne`
`norm_add` 📖	mathematical	`SameRay` `Real` `Real.instCommSemiring` `Real.partialOrder` `Real.instIsStrictOrderedRing` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField`	`Norm.norm` `SeminormedAddCommGroup.toNorm` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Real.instAdd`	—	`Real.instIsStrictOrderedRing` `exists_eq_smul` `add_smul` `norm_smul_of_nonneg` `add_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `add_mul` `Distrib.rightDistribClass`
`norm_eq_iff` 📖	mathematical	`SameRay` `Real` `Real.instCommSemiring` `Real.partialOrder` `Real.instIsStrictOrderedRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField`	`Norm.norm` `NormedAddCommGroup.toNorm`	—	`Real.instIsStrictOrderedRing` `eq_of_norm_eq`
`norm_smul_eq` 📖	mathematical	`SameRay` `Real` `Real.instCommSemiring` `Real.partialOrder` `Real.instIsStrictOrderedRing` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField`	`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` `Norm.norm` `SeminormedAddCommGroup.toNorm`	—	`Real.instIsStrictOrderedRing` `exists_eq_smul` `norm_smul_of_nonneg` `SemigroupAction.mul_smul` `SMulCommClass.smul_comm` `smulCommClass_self`
`norm_sub` 📖	mathematical	`SameRay` `Real` `Real.instCommSemiring` `Real.partialOrder` `Real.instIsStrictOrderedRing` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField`	`Norm.norm` `SeminormedAddCommGroup.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `abs` `Real.lattice` `Real.instAddGroup` `Real.instSub`	—	`Real.instIsStrictOrderedRing` `exists_eq_smul` `sub_smul` `norm_smul_of_nonneg` `sub_nonneg` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `sub_mul` `abs_of_nonneg` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `norm_nonneg` `norm_sub_rev` `abs_sub_comm` `sameRay_comm` `le_of_not_ge`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`norm_injOn_ray_left` 📖	mathematical	—	`Set.InjOn` `Real` `Norm.norm` `NormedAddCommGroup.toNorm` `setOf` `SameRay` `Real.instCommSemiring` `Real.partialOrder` `Real.instIsStrictOrderedRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField`	—	`Real.instIsStrictOrderedRing` `SameRay.exists_nonneg_left` `Real.norm_of_nonneg` `mul_left_inj'` `IsCancelMulZero.toIsRightCancelMulZero` `IsDomain.toIsCancelMulZero` `Real.instIsDomain` `norm_ne_zero_iff` `norm_smul` `NormedSpace.toNormSMulClass`
`norm_injOn_ray_right` 📖	mathematical	—	`Set.InjOn` `Real` `Norm.norm` `NormedAddCommGroup.toNorm` `setOf` `SameRay` `Real.instCommSemiring` `Real.partialOrder` `Real.instIsStrictOrderedRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField`	—	`Real.instIsStrictOrderedRing` `norm_injOn_ray_left`
`not_sameRay_iff_of_norm_eq` 📖	mathematical	`Norm.norm` `NormedAddCommGroup.toNorm`	`SameRay` `Real` `Real.instCommSemiring` `Real.partialOrder` `Real.instIsStrictOrderedRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField`	—	`Iff.not` `Real.instIsStrictOrderedRing` `sameRay_iff_of_norm_eq`
`sameRay_iff_inv_norm_smul_eq` 📖	mathematical	—	`SameRay` `Real` `Real.instCommSemiring` `Real.partialOrder` `Real.instIsStrictOrderedRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `Real.instInv` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`Real.instIsStrictOrderedRing` `eq_or_ne` `norm_zero` `inv_zero` `smul_zero` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `Real.instIsDomain` `GroupWithZero.toNoZeroSMulDivisors` `IsDomain.toIsCancelMulZero` `sameRay_iff_inv_norm_smul_eq_of_ne`
`sameRay_iff_inv_norm_smul_eq_of_ne` 📖	mathematical	—	`SameRay` `Real` `Real.instCommSemiring` `Real.partialOrder` `Real.instIsStrictOrderedRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `Real.instInv` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`Real.instIsStrictOrderedRing` `inv_smul_eq_iff₀` `norm_ne_zero_iff` `SMulCommClass.smul_comm` `smulCommClass_self` `sameRay_iff_norm_smul_eq`
`sameRay_iff_norm_smul_eq` 📖	mathematical	—	`SameRay` `Real` `Real.instCommSemiring` `Real.partialOrder` `Real.instIsStrictOrderedRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`Real.instIsStrictOrderedRing` `SameRay.norm_smul_eq` `norm_pos_iff`
`sameRay_iff_of_norm_eq` 📖	mathematical	`Norm.norm` `NormedAddCommGroup.toNorm`	`SameRay` `Real` `Real.instCommSemiring` `Real.partialOrder` `Real.instIsStrictOrderedRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField`	—	`Real.instIsStrictOrderedRing` `eq_or_ne` `SameRay.zero_right` `norm_eq_zero` `norm_zero` `norm_injOn_ray_right` `SameRay.rfl`

---

← Back to Index