Documentation Verification Report

Basic

📁 Source: Mathlib/Geometry/Polygon/Basic.lean

Statistics

Metric	Count
Definitions `toPolygon`, `Polygon`, `HasNondegenerateEdges`, `HasNondegenerateVertices`, `boundary`, `edgePath`, `edgeSet`, `instCoeFunForallFin`, `toTriangle`, `vertices`	10
Theorems `toPolygon_hasNondegenerateVertices`, `toPolygon_toTriangle`, `toPolygon_vertices`, `two_le`, `hasNondegenerateEdges`, `three_le`, `edgeSet_eq_image_edgePath`, `toTriangle_points`, `toTriangle_toPolygon`	9
Total	19

Affine.Triangle

Definitions

Name	Category	Theorems
`toPolygon` 📖	CompOp	4 math math: `toPolygon_vertices`, `toPolygon_toTriangle`, `Polygon.toTriangle_toPolygon`, `toPolygon_hasNondegenerateVertices`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toPolygon_hasNondegenerateVertices` 📖	mathematical	—	`Polygon.HasNondegenerateVertices` `DFunLike.coe` `Function.Embedding` `Affine.Triangle` `Polygon` `Function.instFunLikeEmbedding` `toPolygon`	—	`Affine.Simplex.independent` `Fintype.complete` `AffineIndependent.comm_right` `AffineIndependent.comm_left`
`toPolygon_toTriangle` 📖	mathematical	—	`Polygon.toTriangle` `DFunLike.coe` `Function.Embedding` `Affine.Triangle` `Polygon` `Function.instFunLikeEmbedding` `toPolygon` `toPolygon_hasNondegenerateVertices`	—	`toPolygon_hasNondegenerateVertices`
`toPolygon_vertices` 📖	mathematical	—	`Polygon.vertices` `DFunLike.coe` `Function.Embedding` `Affine.Triangle` `Polygon` `Function.instFunLikeEmbedding` `toPolygon` `Affine.Simplex.points`	—	—

Polygon

Definitions

Name	Category	Theorems
`HasNondegenerateEdges` 📖	MathDef	1 math math: `HasNondegenerateVertices.hasNondegenerateEdges`
`HasNondegenerateVertices` 📖	MathDef	1 math math: `Affine.Triangle.toPolygon_hasNondegenerateVertices`
`boundary` 📖	CompOp	—
`edgePath` 📖	CompOp	1 math math: `edgeSet_eq_image_edgePath`
`edgeSet` 📖	CompOp	1 math math: `edgeSet_eq_image_edgePath`
`instCoeFunForallFin` 📖	CompOp	—
`toTriangle` 📖	CompOp	3 math math: `toTriangle_points`, `Affine.Triangle.toPolygon_toTriangle`, `toTriangle_toPolygon`
`vertices` 📖	CompOp	2 math math: `toTriangle_points`, `Affine.Triangle.toPolygon_vertices`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`edgeSet_eq_image_edgePath` 📖	mathematical	—	`edgeSet` `Set.image` `DFunLike.coe` `AffineMap` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AffineMap.instFunLike` `edgePath` `Set.Icc` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	—
`toTriangle_points` 📖	mathematical	`HasNondegenerateVertices`	`Affine.Simplex.points` `toTriangle` `vertices`	—	—
`toTriangle_toPolygon` 📖	mathematical	`HasNondegenerateVertices`	`DFunLike.coe` `Function.Embedding` `Affine.Triangle` `Polygon` `Function.instFunLikeEmbedding` `Affine.Triangle.toPolygon` `toTriangle`	—	—

Polygon.HasNondegenerateEdges

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`two_le` 📖	—	`Polygon.HasNondegenerateEdges`	—	—	`finRotate_one` `le_antisymm` `Mathlib.Tactic.IntervalCases.of_lt_right` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_ofNat`

Polygon.HasNondegenerateVertices

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasNondegenerateEdges` 📖	mathematical	`Polygon.HasNondegenerateVertices`	`Polygon.HasNondegenerateEdges`	—	`Fin.neZero` `finRotate_apply` `AffineIndependent.injective`
`three_le` 📖	—	`Polygon.HasNondegenerateVertices`	—	—	`Polygon.HasNondegenerateEdges.two_le` `hasNondegenerateEdges` `AffineIndependent.injective` `zero_add` `add_zero` `le_antisymm` `Mathlib.Tactic.IntervalCases.of_lt_right` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.IntervalCases.of_le_left`

(root)

Definitions

Name	Category	Theorems
`Polygon` 📖	CompData	4 math math: `Affine.Triangle.toPolygon_vertices`, `Affine.Triangle.toPolygon_toTriangle`, `Polygon.toTriangle_toPolygon`, `Affine.Triangle.toPolygon_hasNondegenerateVertices`

---

← Back to Index