Revision #3410 → #4000 · back to history
modifiedInfinite Ramsey theorem113a4c7e232d
| Field | From #3410 | To #4000 |
|---|
| mathlib.decl | exists_increasing_or_nonincreasing_subseq | — |
| mathlib.module | Mathlib.Order.OrderIsoNat | — |
| note | Mathlib has the infinitary Erdős–Szekeres lemma (a special-case relative of infinite Ramsey for pairs) but not the general infinite Ramsey theorem for colourings of subsets. | The general infinite Ramsey theorem for c-colourings of n-element subsets of an infinite set is not formalized in Mathlib; the previously suggested `exists_increasing_or_nonincreasing_subseq` is the infinite Erdős–Szekeres lemma for sequences, not the Ramsey statement. |
| provenance | ai | ai-moderated |
| status | partial | not_formalized |
modifiedm-hypergrapha82cbf09c8cc
| Field | From #3410 | To #4000 |
|---|
| mathlib.decl | Hypergraph | — |
| mathlib.match_kind | generalization | — |
| mathlib.module | Mathlib.Combinatorics.Hypergraph.Basic | — |
| note | Mathlib has a general `Hypergraph` type but no m-uniform restriction defining an m-hypergraph specifically. | Mathlib has no general `Hypergraph` type nor an m-uniform hypergraph definition matching this notion. |
| provenance | ai | ai-moderated |
| status | partial | not_formalized |