Revision #1640 → #2258 · back to history
modifiedTriangle236e9af2bcfd
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | Affine.Triangle |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic |
| note | — | Affine.Triangle abbreviates `Affine.Simplex k P 2`, a bundled triple of affinely independent points. |
| status | — | formalized |
modifiedSum of angles equals straight angle10e647e6b05e
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | EuclideanGeometry.angle_add_angle_add_angle_eq_pi |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Geometry.Euclidean.Triangle |
| note | — | Proves ∠p₁p₂p₃ + ∠p₂p₃p₁ + ∠p₃p₁p₂ = π for three points in a Euclidean affine space. |
| status | — | formalized |
modifiedArea equals half base times height24a1c70f3a59
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No `Affine.Triangle.area` (or simplex analogue with the ½·base·height formula) appears in Mathlib. |
| status | — | not_formalized |
modifiedThree non-collinear points determine a triangled4ef29f02a80
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | Affine.Triangle |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic |
| note | — | The structure `Affine.Triangle` bundles exactly three affinely independent (i.e. non-collinear) points. |
| status | — | formalized |
addedTetrahedrond1a9916474fe
addedSpherical and hyperbolic triangles (non-Euclidean)cc40605372fb
modifiedGeodesic triangle1a0ddcdebdad
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Mathlib has no notion of geodesic triangle on a surface or in a metric space. |
| status | — | not_formalized |
modifiedCurvilinear trianglec35f5118be51
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No definition of curvilinear triangle exists in Mathlib. |
| status | — | not_formalized |
modifiedTriangle (sides and vertices)fb494d910ada
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | Affine.Triangle |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic |
| note | — | Triangles in Mathlib are bundled as three affinely independent vertices, with `Polygon.toTriangle` linking to the three-segment view. |
| status | — | formalized |
modifiedEquilateral, isosceles, scalene trianglesf5557d89390b
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | Affine.Simplex.Equilateral |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.Analysis.Normed.Affine.Simplex |
| note | — | `Affine.Simplex.Equilateral` and `Affine.Simplex.Scalene` exist for simplices, but Mathlib has no `Isosceles` predicate. |
| status | — | partial |
modifiedRight, acute, obtuse trianglesd26ad9729740
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | Affine.Simplex.AcuteAngled |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.Geometry.Euclidean.Simplex |
| note | — | Only `AcuteAngled` (with `Affine.Triangle.acuteAngled_iff_angle_lt`) is in Mathlib; no `Right` or `Obtuse` triangle predicate. |
| status | — | partial |
addedDeltahedron901fffd796dd
addedSimplex (generalized triangle)c8b2963d477e
modifiedCeva's theorem02eb51094fd4
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | Affine.Triangle.prod_div_one_sub_eq_one_of_mem_line_point_lineMap |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.LinearAlgebra.AffineSpace.Ceva |
| note | — | Mathlib has Ceva's theorem for triangles in several equivalent forms (weights, divisions, distances). |
| status | — | formalized |
modifiedMenelaus' theorema4f870cf4f5c
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Grep over Mathlib finds no occurrence of Menelaus. |
| status | — | not_formalized |
modifiedPerpendicular bisector2502b3e23891
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | AffineSubspace.perpBisector |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Geometry.Euclidean.PerpBisector |
| note | — | `perpBisector p₁ p₂` is the perpendicular bisector of the segment [p₁, p₂] as a bundled affine subspace. |
| status | — | formalized |
modifiedCircumcenter from perpendicular bisectorse2a6c6caa38a
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | Affine.Simplex.circumcenter |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.Geometry.Euclidean.Circumcenter |
| note | — | Circumcenter is defined via uniqueness of an equidistant point; the explicit concurrence-of-perpBisectors theorem isn't stated as such. |
| status | — | partial |
addedCircumcircled9465424012e
modifiedThales' theorem (circumcenter on side)7e33379261b4
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | EuclideanGeometry.Sphere.thales_theorem |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Geometry.Euclidean.Angle.Sphere |
| note | — | An inscribed angle subtending a diameter is a right angle; aliased as `thales_theorem`. |
| status | — | formalized |
modifiedCircumcenter location and triangle type16f2854c044f
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No lemma classifying triangle type by interior/exterior position of the circumcenter is in Mathlib. |
| status | — | not_formalized |
modifiedAltitude of a trianglefe7a848f807c
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | Affine.Simplex.altitude |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.Geometry.Euclidean.Altitude |
| note | — | Altitude of a simplex is defined as the line through a vertex orthogonal to the opposite face. |
| status | — | formalized |
modifiedOrthocenter from altitudes2f55d550049d
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | Affine.Triangle.eq_orthocenter_of_forall_mem_altitude |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Geometry.Euclidean.MongePoint |
| note | — | `orthocenter_mem_altitude` plus `eq_orthocenter_of_forall_mem_altitude` show the three altitudes concur at the orthocenter. |
| status | — | formalized |
modifiedOrthocenter inside iff acute37a6e3bd928b
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Mathlib has the orthocenter and AcuteAngled but no lemma linking the orthocenter's interior position to acuteness. |
| status | — | not_formalized |
modifiedAngle bisectorfd0546b7265c
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No dedicated `angleBisector` definition appears in Mathlib's geometry library. |
| status | — | not_formalized |
modifiedIncenter from angle bisectors2ee9902a4aca
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | Affine.Simplex.incenter |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.Geometry.Euclidean.Incenter |
| note | — | Incenter is defined as the center of the insphere (tangent to the faces), not via concurrence of angle bisectors. |
| status | — | partial |
addedIncircle586a53147c44
modifiedExcircles and orthocentric system65621c6252a3
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | Affine.Simplex.exsphere |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.Geometry.Euclidean.Incenter |
| note | — | `exsphere` covers excircles, and `EuclideanGeometry.OrthocentricSystem` formalises the orthocentric system. |
| status | — | formalized |
modifiedNine-point circle18ff01a2a164
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | Affine.Simplex.ninePointCircle |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Geometry.Euclidean.NinePointCircle |
| note | — | Nine-point circle defined; lemmas like `faceOppositeCentroid_mem_ninePointCircle` and `altitudeFoot_mem_ninePointCircle` verify the nine points. |
| status | — | formalized |
addedNine-point circle radius is half circumradiusf763d9301591
addedFeuerbach's theorem (nine-point circle touches incircle and excircles)a9b538321f42
modifiedEuler's line482d05f21781
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Circumcenter, centroid and orthocenter all exist but the collinearity result `EulerLine` is not stated in Mathlib. |
| status | — | not_formalized |
addedDistances along Euler's line7ca6d05563d5
modifiedMedian of a triangle8a6747ab4880
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | Affine.Simplex.median |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid |
| note | — | `median` is the line from a vertex of a simplex through the centroid of the opposite face; for a triangle this is the median through the midpoint. |
| status | — | formalized |
modifiedCentroid from medians86d874ea8c89
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | Affine.Simplex.eq_centroid_of_forall_mem_median |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid |
| note | — | States that any point lying on all medians of a simplex equals the centroid. |
| status | — | formalized |
addedCentroid is center of mass4df51d9c70cc
modifiedCentroid cuts median 2:1837031c29f57
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | Affine.Simplex.point_vsub_centroid_eq_smul_vsub |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid |
| note | — | Commandino's theorem: vertex-to-centroid equals `n` times centroid-to-faceOppositeCentroid, giving the 2:1 ratio when n = 2. |
| status | — | formalized |
modifiedSymmedian and symmedian pointaafac5de5bea
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No symmedian or symmedian point definition exists in Mathlib. |
| status | — | not_formalized |
modifiedSum of interior angles is 180°b9e51ac5d7cc
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | EuclideanGeometry.angle_add_angle_add_angle_eq_pi |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Geometry.Euclidean.Triangle |
| note | — | Sum of the three angle-at-point measures equals π. |
| status | — | formalized |
addedAngle-sum equivalent to parallel postulate4a766053baf0
modifiedExterior angle theorem4527572f8c73
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | EuclideanGeometry.exterior_angle_eq_angle_add_angle |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Geometry.Euclidean.Triangle |
| note | — | Stated directly using `Sbtw` to place a point on the extension of a side. |
| status | — | formalized |
modifiedSum of exterior angles is 360°58126f9123a9
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No statement summing the three exterior angles to 2π is present in Mathlib. |
| status | — | not_formalized |
modifiedTrigonometric functions in right triangles1c93b21a86ee
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | Real.sin |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic |
| note | — | Mathlib defines sin/cos analytically and has `cos_angle` in terms of inner products, but does not give the right-triangle ratio definition. |
| status | — | partial |
modifiedLaw of sines and cosines062e6192c4e9
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | EuclideanGeometry.law_cos |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Geometry.Euclidean.Triangle |
| note | — | Both `law_cos` and `law_sin` are proved (with vector-angle variants in InnerProductGeometry). |
| status | — | formalized |
modifiedThree angles summing to 180° form a triangle1839d4db151d
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No converse-existence lemma constructing a triangle from three angles summing to π is in Mathlib. |
| status | — | not_formalized |
modifiedDegenerate triangleb0aa8f47ce41
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | `Affine.Triangle` requires affine independence, so a degenerate-triangle predicate is not defined separately. |
| status | — | not_formalized |
modifiedSimilar triangles0b7ecd573adf
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | Similar |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Topology.MetricSpace.Similarity |
| note | — | `Similar` is the general indexed-family similarity used by the triangle similarity lemmas in `Mathlib.Geometry.Euclidean.Similarity`. |
| status | — | formalized |
modifiedAA similarity9e380e19f216
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | EuclideanGeometry.similar_of_angle_angle |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Geometry.Euclidean.Similarity |
| note | — | Two pairs of equal angles imply similarity of the two triangles. |
| status | — | formalized |
modifiedSAS similarityb1a4632a48d6
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | EuclideanGeometry.similar_of_side_angle_side |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Geometry.Euclidean.Similarity |
| note | — | Proportional adjacent sides with equal included angle imply similarity. |
| status | — | formalized |
modifiedSSS similarity407034261b14
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | similar_of_side_side |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Topology.MetricSpace.Similarity |
| note | — | Proportional sides imply similarity for the (a,b,c)/(a',b',c') triples. |
| status | — | formalized |
modifiedCongruent trianglesfd6b7c4bd7e9
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | EuclideanGeometry.triangle_congruent_iff_dist_eq |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Geometry.Euclidean.Congruence |
| note | — | Triangle congruence is the specialisation of the general `Congruent` predicate, characterised by pairwise equal distances. |
| status | — | formalized |
modifiedSAS congruence postulateca715ce0dd1f
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | EuclideanGeometry.side_angle_side |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Geometry.Euclidean.Congruence |
| note | — | Two sides and the included angle equal ⇒ triangles congruent. |
| status | — | formalized |
modifiedASA congruence719e124a4df9
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | EuclideanGeometry.angle_side_angle |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Geometry.Euclidean.Congruence |
| note | — | Two angles and the included side equal ⇒ triangles congruent (with a non-collinearity hypothesis). |
| status | — | formalized |
modifiedSSS congruencea9ec7c2c49cd
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | EuclideanGeometry.side_side_side |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Geometry.Euclidean.Congruence |
| note | — | Three equal pairs of sides ⇒ congruent, even for degenerate triangles. |
| status | — | formalized |
modifiedAAS congruence48d4f73eceb3
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | EuclideanGeometry.angle_angle_side |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Geometry.Euclidean.Congruence |
| note | — | Two angles and a non-included side equal ⇒ congruent. |
| status | — | formalized |
modifiedArea as half base times altitude8277edfdb10b
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No `triangle area = ½·base·height` lemma is present in Mathlib. |
| status | — | not_formalized |
modifiedArea from two sides and included angled79217ad3f65
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No `½ a b sin C` triangle-area formula in Mathlib. |
| status | — | not_formalized |
modifiedHeron's formulaeb36da31cea6
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No Heron's-formula declaration appears in Mathlib (the `Heron`-named hits are all unrelated, e.g. `Harmonic`). |
| status | — | not_formalized |
modifiedAffine relative area39eb65af66c2
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Mathlib does not define a notion of relative/affine triangle area. |
| status | — | not_formalized |
modifiedShoelace formula for triangle areac5c78681fdd9
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Grep for `shoelace`/`Shoelace` finds no Mathlib declaration. |
| status | — | not_formalized |
modifiedTriangle inequalityfe9566631302
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | dist_triangle |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.Topology.MetricSpace.Pseudo.Defs |
| note | — | The metric-space `dist_triangle` is the general form; `norm_add_le` is the vector version. |
| status | — | formalized |
modifiedConverse of triangle inequality830921f2ca5e
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No constructive lemma producing a triangle from three side lengths satisfying the triangle inequality is in Mathlib. |
| status | — | not_formalized |
modifiedTriangle rigidity13ba6912fd15
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | EuclideanGeometry.side_side_side |
| mathlib.match_kind | — | invocation |
| mathlib.module | — | Mathlib.Geometry.Euclidean.Congruence |
| note | — | SSS congruence is the precise statement of triangle rigidity; no separate `rigidity` lemma exists. |
| status | — | partial |
modifiedPolygon triangulation count70b99121289b
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Polygon triangulation, Catalan-number counts, and simple-polygon decomposition are not formalised in Mathlib. |
| status | — | not_formalized |
modifiedTwo ears theoremdc26c7f575de
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Grep finds no `TwoEar`/`ears`-theorem declaration in Mathlib. |
| status | — | not_formalized |
modifiedTrilinear coordinates6e35c8b5ab0a
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Mathlib mentions trilinear coordinates only in a docstring of `SignedDist`; no dedicated definition exists. |
| status | — | not_formalized |
modifiedBarycentric coordinates719774c14add
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | AffineBasis.coord |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.LinearAlgebra.AffineSpace.Basis.Defs |
| note | — | `AffineBasis.coord` gives the ith barycentric coordinate map; lemmas like `coord_apply_combination` characterise it. |
| status | — | formalized |
modifiedUnique incircle59d26382e9da
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | Affine.Simplex.insphere |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.Geometry.Euclidean.Incenter |
| note | — | Mathlib's insphere is uniquely defined for every simplex; specialised to a triangle it gives the unique incircle. |
| status | — | formalized |
modifiedSteiner inellipse17cca5701672
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Grep for `Steiner.*inellipse`/`SteinerInellipse` returns no matches. |
| status | — | not_formalized |
modifiedMarden's theorem1d45afd76896
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No `Marden` declaration in Mathlib. |
| status | — | not_formalized |
addedSteiner inellipse has maximum areaa876dc23fe7a
modifiedMandart inellipse32722cd79009
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Grep for `Mandart` returns no matches. |
| status | — | not_formalized |
modifiedPedal triangle and medial triangle87735ec9b6fd
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Neither `pedalTriangle` nor `medialTriangle` is defined in Mathlib. |
| status | — | not_formalized |
modifiedMedial triangle subdivides into four congruent triangles4d3209c3f568
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Without a medial-triangle definition, the corresponding subdivision lemma is not in Mathlib. |
| status | — | not_formalized |
modifiedIntouch triangle529ddfd67822
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No `intouchTriangle` declaration; only the underlying `Simplex.touchpoint` exists. |
| status | — | not_formalized |
modifiedExtouch trianglef6d144e8df53
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No `extouchTriangle` declaration in Mathlib. |
| status | — | not_formalized |
modifiedCalabi trianglece3b4775086f
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No Calabi triangle definition exists in Mathlib. |
| status | — | not_formalized |
modifiedInscribed squares by triangle type2de49ed23ff0
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No Mathlib lemma counts inscribed squares of a triangle by type. |
| status | — | not_formalized |
modifiedLemoine hexagon98fb603dd729
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No `Lemoine` hexagon definition is present in Mathlib. |
| status | — | not_formalized |
modifiedConvex polygon inscribed in triangle area boundeef08703c1ed
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No area-bound theorem comparing inscribed convex polygons to the enclosing triangle is in Mathlib. |
| status | — | not_formalized |
addedEquality case: inscribed parallelogram3963d1dab959
modifiedTangential triangleba5b68cfe28c
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No `tangentialTriangle` definition exists in Mathlib. |
| status | — | not_formalized |
modifiedSteiner circumellipsedf845ac94542
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Steiner circumellipse is not defined or characterised in Mathlib. |
| status | — | not_formalized |
addedSteiner circumellipse has minimum area428d03d3dc47
modifiedKiepert hyperbolab8eabc430a54
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No Kiepert hyperbola is formalised in Mathlib. |
| status | — | not_formalized |
modifiedMaximum-area triangle in convex polygon2e114d6ecb96
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Algorithmic result on maximum-area inscribed triangles is not part of Mathlib. |
| status | — | not_formalized |
modifiedCircular trianglec1c6185ce9f7
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No circular-triangle definition appears in Mathlib. |
| status | — | not_formalized |
addedIntersection of three disks is a convex circular triangle7f4fbf591f70
modifiedReuleaux triangle36f37cb2d991
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Grep for `Reuleaux` returns no matches. |
| status | — | not_formalized |
modifiedMohr–Mascheroni theorem52dba7200f1a
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No `Mohr` declaration in Mathlib (the `Mascheroni` hits are about the Euler–Mascheroni constant). |
| status | — | not_formalized |
modifiedPseudotriangleca725b91c49b
| Field | From #1640 | To #2258 |
|---|
| anchor.snippet | For | A pseudotriangle is a simply-connected subset of the plane lying between three mutually tangent convex regions |
| kind | proposition | definition |
| label | Pseudo-triangulation counts | Pseudotriangle |
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Mathlib has no notion of pseudotriangle. |
| status | — | not_formalized |
addedPseudo-triangulation counts6e0ffac79180
modifiedConvex hull of pseudotriangle is a trianglec0edc2d91bc2
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Without a pseudotriangle definition, no convex-hull lemma about them is in Mathlib. |
| status | — | not_formalized |
modifiedHyperbolic and spherical triangles6f7e16194078
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No hyperbolic or spherical triangle definition exists in Mathlib. |
| status | — | not_formalized |
modifiedAngle sum in hyperbolic and spherical triangles264543e78a1d
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Mathlib does not formalise angle sums in hyperbolic or spherical triangles. |
| status | — | not_formalized |
modifiedGirard's theorem2d0ae3059e95
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No Girard-theorem (spherical excess) declaration is in Mathlib. |
| status | — | not_formalized |
addedTriangle comparison theorems88288baf6609
modifiedCAT(k) space01a6e4f578b6
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No CAT(k) space definition exists in Mathlib. |
| status | — | not_formalized |
modifiedFractal triangles (Sierpiński, Koch)f9984e748a7f
| Field | From #1640 | To #2258 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Mathlib has no Sierpiński gasket or Koch snowflake construction. |
| status | — | not_formalized |
deletedPseudotriangleb967537f3bd4