Documentation Verification Report

TriangleInequality

📁 Source: Mathlib/Geometry/Euclidean/Angle/Unoriented/TriangleInequality.lean

Statistics

Metric	Count
Definitions	0
Theorems `angle_le_angle_add_angle`, `angle_eq_angle_add_add_angle_add_of_mem_span`, `angle_eq_angle_add_angle_iff`, `angle_le_angle_add_angle`	4
Total	4

EuclideanGeometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`angle_le_angle_add_angle` 📖	mathematical	—	`Real` `Real.instLE` `angle` `Real.instAdd`	—	`InnerProductGeometry.angle_le_angle_add_angle`

InnerProductGeometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`angle_eq_angle_add_add_angle_add_of_mem_span` 📖	mathematical	`Submodule` `NNReal` `instSemiringNNReal` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NNReal.instModuleOfReal` `NormedSpace.toModule` `Real` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set` `Set.instInsert` `Set.instSingletonSet`	`angle` `Real.instAdd`	—	`Submodule.mem_span_pair` `LE.le.eq_or_lt` `zero_le` `NNReal.instCanonicallyOrderedAdd` `zero_smul` `add_zero` `zero_add` `angle_smul_right_of_pos` `angle_smul_left_of_pos` `angle_self` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `Real.instIsDomain` `GroupWithZero.toNoZeroSMulDivisors` `IsDomain.toIsCancelMulZero` `angle_comm` `angle_eq_angle_add_add_angle_add` `smul_ne_zero` `instIsDomain` `LT.lt.ne'` `smul_zero` `add_comm`
`angle_eq_angle_add_angle_iff` 📖	mathematical	—	`angle` `Real` `Real.instAdd` `Real.pi` `Submodule` `NNReal` `instSemiringNNReal` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NNReal.instModuleOfReal` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set` `Set.instInsert` `Set.instSingletonSet`	—	`angle_eq_zero_iff` `CanLift.prf` `NNReal.canLift` `LT.lt.le` `Submodule.smul_mem` `Submodule.mem_span_of_mem` `Nat.instAtLeastTwoHAddOfNat` `angle_zero_left` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `NNReal.smul_def` `Submodule.span_insert_zero` `Submodule.span_singleton_smul_eq` `Nat.cast_zero` `angle_zero_right` `AddRightCancelSemigroup.toIsRightCancelAdd` `NormedSpace.norm_normalize_eq_one_iff` `angle_normalize_right` `angle_normalize_left` `IsScalarTower.left` `angle_eq_angle_add_add_angle_add_of_mem_span`
`angle_le_angle_add_angle` 📖	mathematical	—	`Real` `Real.instLE` `angle` `Real.instAdd`	—	`Nat.instAtLeastTwoHAddOfNat` `angle_zero_left` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `angle_nonneg` `angle_zero_right` `add_halves` `ZeroLEOneClass.neZero.two` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `angle_le_pi` `covariant_swap_add_of_covariant_add` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `angle_normalize_right` `angle_normalize_left` `NormedSpace.norm_normalize_eq_one_iff`

---

← Back to Index