Documentation Verification Report

Simplex

📁 Source: Mathlib/Analysis/Normed/Affine/Simplex.lean

Statistics

Metric	Count
Definitions `Simplex`, `Equilateral`, `Scalene`	3
Theorems `dist_eq`, `equilateral`, `dist_ne`, `equilateral_reindex_iff`, `regular_reindex_iff`, `scalene_reindex_iff`, `equilateral_iff_dist_01_eq_02_and_dist_01_eq_12`, `equilateral_iff_dist_eq_and_dist_eq`, `scalene_iff_dist_ne_and_dist_ne_and_dist_ne`	9
Total	12

Affine

Definitions

Name	Category	Theorems
`Simplex` 📖	CompData	1 math math: `Simplex.nonempty`

Affine.Simplex

Definitions

Name	Category	Theorems
`Equilateral` 📖	MathDef	4 math math: `Affine.Triangle.equilateral_iff_dist_01_eq_02_and_dist_01_eq_12`, `Regular.equilateral`, `equilateral_reindex_iff`, `Affine.Triangle.equilateral_iff_dist_eq_and_dist_eq`
`Scalene` 📖	MathDef	2 math math: `scalene_reindex_iff`, `Affine.Triangle.scalene_iff_dist_ne_and_dist_ne_and_dist_ne`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equilateral_reindex_iff` 📖	mathematical	—	`Equilateral` `reindex` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddTorsor.toAddTorsor`	—	`Equiv.symm_apply_apply` `Equiv.injective`
`regular_reindex_iff` 📖	mathematical	—	`Regular` `reindex` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddTorsor.toAddTorsor`	—	`Equiv.symm_apply_apply` `Equiv.apply_symm_apply`
`scalene_reindex_iff` 📖	mathematical	—	`Scalene` `reindex` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddTorsor.toAddTorsor`	—	`Ne.lt_of_le` `Equiv.injective` `LT.lt.ne'` `not_lt` `Equiv.symm_apply_apply` `Equiv.apply_symm_apply` `dist_comm` `Function.Injective.of_comp_iff'` `Equiv.bijective`

Affine.Simplex.Equilateral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dist_eq` 📖	mathematical	`Affine.Simplex.Equilateral`	`Dist.dist` `PseudoMetricSpace.toDist` `Affine.Simplex.points` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddTorsor.toAddTorsor`	—	—

Affine.Simplex.Regular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equilateral` 📖	mathematical	`Affine.Simplex.Regular`	`Affine.Simplex.Equilateral`	—	`dist_comm` `IsometryEquiv.dist_eq` `Equiv.swap_apply_left` `Equiv.swap_apply_of_ne_of_ne`

Affine.Simplex.Scalene

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dist_ne` 📖	—	`Affine.Simplex.Scalene`	—	—	`Ne.lt_or_gt` `dist_comm`

Affine.Triangle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equilateral_iff_dist_01_eq_02_and_dist_01_eq_12` 📖	mathematical	—	`Affine.Simplex.Equilateral` `Dist.dist` `PseudoMetricSpace.toDist` `Affine.Simplex.points` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddTorsor.toAddTorsor`	—	`equilateral_iff_dist_eq_and_dist_eq`
`equilateral_iff_dist_eq_and_dist_eq` 📖	mathematical	—	`Affine.Simplex.Equilateral` `Dist.dist` `PseudoMetricSpace.toDist` `Affine.Simplex.points` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddTorsor.toAddTorsor`	—	`dist_comm`
`scalene_iff_dist_ne_and_dist_ne_and_dist_ne` 📖	mathematical	—	`Affine.Simplex.Scalene`	—	`Affine.Simplex.Scalene.dist_ne` `Fintype.complete`

---

← Back to Index