Revision #1522 → #1790 · back to history
addedR(3,3) > 5 (K_5 has a triangle-free 2-colouring)e60d8ab6cef9
addedParty problem interpretation of R(m,n)f6f8a2babf95
addedPaley graph of order 17 is unique (4,4,17) graphd9083fc11eb2
addedBurr–Erdős conjecture (proven)c71d236135b3
modifiedm-hypergrapha82cbf09c8cc
| Field | From #1522 | To #1790 |
|---|
| mathlib.decl | — | Hypergraph |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.Combinatorics.Hypergraph.Basic |
| note | Mathlib has SimpleGraph but no m-uniform hypergraph type matching this definition. | Mathlib has a general `Hypergraph` type but no m-uniform restriction defining an m-hypergraph specifically. |
| status | not_formalized | partial |
modifiedΣ-bounding schemae6b6d276857d
| Field | From #1522 | To #1790 |
|---|
| anchors | [{"section":"Reverse mathematics","snippet":"Intuitively, it says that if"},{"type":"math_alttext","value":"{\\displaystyle \\forall n[\\forall i<n\\exists k,\\phi (i,k)\\to \\exists b\\forall i<n\\exists k<b,\\phi (i,k)]}"}] | — |
| provenance | ai | ai-moderated |