Documentation Verification Report

StrictConvexBetween

📁 Source: Mathlib/Analysis/Convex/StrictConvexBetween.lean

Statistics

Metric	Count
Definitions `affineIsometryOfStrictConvexSpace`	1
Theorems `sbtw_of_dist_eq_of_dist_lt`, `wbtw_of_dist_eq_of_dist_le`, `affineIsometryOfStrictConvexSpace_apply`, `coe_affineIsometryOfStrictConvexSpace`, `dist_lt_max_dist`, `dist_le_max_dist`, `dist_add_dist_eq_iff`, `dist_lt_dist_add_dist_iff`, `eq_lineMap_of_dist_eq_mul_of_dist_eq_mul`, `eq_midpoint_of_dist_eq_half`	10
Total	11

Collinear

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sbtw_of_dist_eq_of_dist_lt` 📖	mathematical	`Collinear` `Real` `Real.instDivisionRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedAddTorsor.toAddTorsor` `Set` `Set.instInsert` `Set.instSingletonSet` `Dist.dist` `PseudoMetricSpace.toDist` `Real.instLT`	`Sbtw` `Real.instRing` `Real.partialOrder`	—	`wbtw_of_dist_eq_of_dist_le` `LT.lt.le` `LT.lt.ne`
`wbtw_of_dist_eq_of_dist_le` 📖	mathematical	`Collinear` `Real` `Real.instDivisionRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedAddTorsor.toAddTorsor` `Set` `Set.instInsert` `Set.instSingletonSet` `Dist.dist` `PseudoMetricSpace.toDist` `Real.instLE`	`Wbtw` `Real.instRing` `Real.partialOrder`	—	`wbtw_or_wbtw_or_wbtw` `Real.instIsStrictOrderedRing` `Real.instIsOrderedRing` `Sbtw.dist_lt_max_dist` `LE.le.not_gt` `lt_self_iff_false` `lt_max_iff`

Isometry

Definitions

Name	Category	Theorems
`affineIsometryOfStrictConvexSpace` 📖	CompOp	2 math math: `coe_affineIsometryOfStrictConvexSpace`, `affineIsometryOfStrictConvexSpace_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`affineIsometryOfStrictConvexSpace_apply` 📖	mathematical	`Isometry` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace`	`DFunLike.coe` `AffineIsometry` `Real` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `MetricSpace.toPseudoMetricSpace` `AffineIsometry.instFunLike` `affineIsometryOfStrictConvexSpace`	—	—
`coe_affineIsometryOfStrictConvexSpace` 📖	mathematical	`Isometry` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace`	`DFunLike.coe` `AffineIsometry` `Real` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `MetricSpace.toPseudoMetricSpace` `AffineIsometry.instFunLike` `affineIsometryOfStrictConvexSpace`	—	—

Sbtw

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dist_lt_max_dist` 📖	mathematical	`Sbtw` `Real` `Real.instRing` `Real.partialOrder` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedAddTorsor.toAddTorsor`	`Real.instLT` `Dist.dist` `PseudoMetricSpace.toDist` `Real.instMax`	—	`left_ne_right` `Real.instIsOrderedRing` `Set.mem_insert_iff` `insert_endpoints_openSegment` `Real.instZeroLEOneClass` `affineSegment_eq_segment` `Wbtw.eq_1` `wbtw_vsub_const_iff` `eq_1` `vsub_left_cancel_iff` `Set.mem_image` `openSegment_eq_image` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `dist_eq_norm_vsub` `norm_combo_lt_of_ne` `le_max_left` `le_max_right` `sub_pos` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.term_add_termg` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Meta.NormNum.isInt_neg` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Abel.zero_termg`

Wbtw

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dist_le_max_dist` 📖	mathematical	`Wbtw` `Real` `Real.instRing` `Real.partialOrder` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedAddTorsor.toAddTorsor`	`Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `Real.instMax`	—	`LT.lt.le` `Sbtw.dist_lt_max_dist`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dist_add_dist_eq_iff` 📖	mathematical	—	`Real` `Real.instAdd` `Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace` `Wbtw` `Real.instRing` `Real.partialOrder` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedAddTorsor.toAddTorsor`	—	`dist_eq_norm'` `Real.instIsStrictOrderedRing` `sub_add_sub_cancel'` `Function.Injective.mem_set_image` `vsub_left_injective` `Real.instIsOrderedRing` `dist_vsub_cancel_right`
`dist_lt_dist_add_dist_iff` 📖	mathematical	—	`Real` `Real.instLT` `Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace` `Real.instAdd` `Wbtw` `Real.instRing` `Real.partialOrder` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedAddTorsor.toAddTorsor`	—	`ne_iff_lt_iff_le` `dist_triangle` `not_iff_not` `dist_add_dist_eq_iff`
`eq_lineMap_of_dist_eq_mul_of_dist_eq_mul` 📖	mathematical	`Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace` `Real` `Real.instMul` `Real.instSub` `Real.instOne`	`DFunLike.coe` `AffineMap` `Real.instRing` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedAddTorsor.toAddTorsor` `AffineMap.instFunLike` `AffineMap.lineMap`	—	`mem_segment_iff_wbtw` `Real.instIsOrderedRing` `dist_add_dist_eq_iff` `dist_zero` `dist_vsub_cancel_right` `dist_eq_norm_vsub'` `add_mul` `Distrib.rightDistribClass` `add_sub_cancel` `one_mul` `eq_or_ne` `AffineMap.lineMap_same` `vsub_self` `segment_same` `Real.instZeroLEOneClass` `zero_add` `smul_zero` `AffineMap.lineMap_apply` `mul_left_inj'` `IsCancelMulZero.toIsRightCancelMulZero` `IsDomain.toIsCancelMulZero` `Real.instIsDomain` `dist_ne_zero` `Real.norm_of_nonneg` `norm_smul` `NormedSpace.toNormSMulClass` `vsub_vadd`
`eq_midpoint_of_dist_eq_half` 📖	mathematical	`Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`midpoint` `Real.instRing` `invertibleTwo` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real.instField` `IsStrictOrderedRing.toCharZero` `DivisionSemiring.toSemiring` `Real.partialOrder` `Real.instIsStrictOrderedRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedAddTorsor.toAddTorsor`	—	`Nat.instAtLeastTwoHAddOfNat` `eq_lineMap_of_dist_eq_mul_of_dist_eq_mul` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `invOf_eq_inv` `div_eq_inv_mul` `one_div` `sub_half` `CharZero.NeZero.two`

---

← Back to Index