Revision #2742 → #3737 · back to history
modifiedConvex combinations stay in Se47a1c70279b
| Field | From #2742 | To #3737 |
|---|
| anchors | [{"section":"Properties","snippet":"Given r points u 1 , ..., u r in a convex set S"},{"type":"math_alttext","value":"{\\displaystyle \\sum _{k=1}^{r}\\lambda _{k}u_{k}}"}] | — |
modifiedConvex body27abd0136e20
| Field | From #2742 | To #3737 |
|---|
| anchors | [{"section":"Convex sets and rectangles","snippet":"Let C be a convex body in the plane (a convex set whose interior is non-empty)"},{"type":"math_alttext","value":"{\\displaystyle {\\tfrac {1}{2}}\\cdot \\operatorname {Area} (R)\\leq \\operatorname {Area} (C)\\leq 2\\cdot \\operatorname {Area} (r)}"}] | — |
modifiedInscribed/circumscribed rectanglef6e6cc6f5215
| Field | From #2742 | To #3737 |
|---|
| anchors | [{"section":"Convex sets and rectangles","snippet":"We can inscribe a rectangle r in C such that a homothetic copy R of r is circumscribed about C"},{"type":"math_alttext","value":"{\\displaystyle {\\tfrac {1}{2}}\\cdot \\operatorname {Area} (R)\\leq \\operatorname {Area} (C)\\leq 2\\cdot \\operatorname {Area} (r)}"}] | — |
modifiedParameterization of planar convex bodies5eaa79cf6a8e
| Field | From #2742 | To #3737 |
|---|
| anchors | [{"section":"Blaschke-Santaló diagrams","snippet":"can be parameterized in terms of the convex body diameter D"},{"type":"math_alttext","value":"{\\displaystyle 2r\\leq D\\leq 2R}"},{"type":"math_alttext","value":"{\\displaystyle R\\leq {\\frac {\\sqrt {3}}{3}}D}"},{"type":"math_alttext","value":"{\\displaystyle r+R\\leq D}"},{"type":"math_alttext","value":"{\\displaystyle D^{2}{\\sqrt {4R^{2}-D^{2}}}\\leq 2R(2R+{\\sqrt {4R^{2}-D^{2}}})}"}] | — |
modifiedBlaschke–Santaló diagram3154fc179f31
| Field | From #2742 | To #3737 |
|---|
| anchors | [{"section":"Blaschke-Santaló diagrams","snippet":"is known a ( r , D , R ) Blachke-Santaló diagram"},{"type":"math_alttext","value":"{\\displaystyle 2r\\leq D\\leq 2R}"},{"type":"math_alttext","value":"{\\displaystyle R\\leq {\\frac {\\sqrt {3}}{3}}D}"},{"type":"math_alttext","value":"{\\displaystyle r+R\\leq D}"},{"type":"math_alttext","value":"{\\displaystyle D^{2}{\\sqrt {4R^{2}-D^{2}}}\\leq 2R(2R+{\\sqrt {4R^{2}-D^{2}}})}"}] | — |
modifiedConvex sets form a latticeb222871e4857
| Field | From #2742 | To #3737 |
|---|
| anchors | [{"section":"Convex hulls","snippet":"is needed for the set of convex sets to form a lattice"},{"type":"math_alttext","value":"{\\displaystyle \\operatorname {Conv} (S)\\vee \\operatorname {Conv} (T)=\\operatorname {Conv} (S\\cup T)=\\operatorname {Conv} {\\bigl (}\\operatorname {Conv} (S)\\cup \\operatorname {Conv} (T){\\bigr )}.}"}] | — |
modifiedConvex subsets form a complete lattice8734b8164a56
| Field | From #2742 | To #3737 |
|---|
| anchors | [{"section":"Convex hulls","snippet":"form a complete lattice"},{"type":"math_alttext","value":"{\\displaystyle \\operatorname {Conv} (S)\\vee \\operatorname {Conv} (T)=\\operatorname {Conv} (S\\cup T)=\\operatorname {Conv} {\\bigl (}\\operatorname {Conv} (S)\\cup \\operatorname {Conv} (T){\\bigr )}.}"}] | — |
modifiedMinkowski sum of two sets3e2c889572c0
| Field | From #2742 | To #3737 |
|---|
| anchors | [{"section":"Minkowski addition","snippet":"the Minkowski sum of two (non-empty) sets"},{"type":"math_alttext","value":"{\\displaystyle S_{1}+S_{2}=\\{x_{1}+x_{2}:x_{1}\\in S_{1},x_{2}\\in S_{2}\\}.}"},{"type":"math_alttext","value":"{\\displaystyle \\sum _{n}S_{n}=\\left\\{\\sum _{n}x_{n}:x_{n}\\in S_{n}\\right\\}.}"}] | — |
modifiedMinkowski sum of a finite family7018b1e3ed35
| Field | From #2742 | To #3737 |
|---|
| anchors | [{"section":"Minkowski addition","snippet":"the Minkowski sum of a finite family of (non-empty) sets"},{"type":"math_alttext","value":"{\\displaystyle S_{1}+S_{2}=\\{x_{1}+x_{2}:x_{1}\\in S_{1},x_{2}\\in S_{2}\\}.}"},{"type":"math_alttext","value":"{\\displaystyle \\sum _{n}S_{n}=\\left\\{\\sum _{n}x_{n}:x_{n}\\in S_{n}\\right\\}.}"}] | — |
modifiedZero set is the identity element9aad55a493ee
| Field | From #2742 | To #3737 |
|---|
| anchors | [{"section":"Minkowski addition","snippet":"is the identity element of Minkowski addition"},{"type":"math_alttext","value":"{\\displaystyle S+\\{0\\}=S;}"}] | — |
modifiedConvex hull of Minkowski sum6a967aa269ea
| Field | From #2742 | To #3737 |
|---|
| anchors | [{"section":"Convex hulls of Minkowski sums","snippet":"the convex hull of their Minkowski sum is the Minkowski sum of their convex hulls"},{"type":"math_alttext","value":"{\\displaystyle \\operatorname {Conv} (S_{1}+S_{2})=\\operatorname {Conv} (S_{1})+\\operatorname {Conv} (S_{2}).}"}] | — |
modifiedFinite-collection versionc4bc434b5e0b
| Field | From #2742 | To #3737 |
|---|
| anchors | [{"section":"Convex hulls of Minkowski sums","snippet":"This result holds more generally for each finite collection of non-empty sets"},{"type":"math_alttext","value":"{\\displaystyle {\\text{Conv}}\\left(\\sum _{n}S_{n}\\right)=\\sum _{n}{\\text{Conv}}\\left(S_{n}\\right).}"}] | — |
modifiedRecession conef43d4b312aa4
| Field | From #2742 | To #3737 |
|---|
| anchors | [{"section":"Minkowski sums of convex sets","snippet":"the concept of a recession cone of a non-empty convex subset S"},{"type":"math_alttext","value":"{\\displaystyle \\operatorname {rec} S=\\left\\{x\\in X\\,:\\,x+S\\subseteq S\\right\\},}"},{"type":"math_alttext","value":"{\\displaystyle \\operatorname {rec} S=\\bigcap _{t>0}t(S-s_{0}).}"}] | — |
| mathlib.decl | asymptoticCone | — |
| mathlib.module | Mathlib.Topology.Algebra.AsymptoticCone | — |
| note | Mathlib's `asymptoticCone` corresponds to the recession cone for closed convex sets but is defined via filters rather than as the textbook recession cone. | Mathlib has no dedicated `recessionCone` / `rec S` definition for convex sets; the prior `asymptoticCone` pointer does not identify a real Mathlib declaration. |
| provenance | ai | ai-moderated |
| status | partial | not_formalized |
addedTrivial faces of a convex setb461991c5a46