73_ascending_descending_sequences): Erdős–Szekeres (#3074)

Commit

5 years ago

feat(archive/100-theorems-list/73_ascending_descending_sequences): Erdős–Szekeres (#3074) Prove the Erdős-Szekeres theorem on ascending or descending sequences

Author

b-mehta

Parents

5c7e1a22

mathlib e1a72b50 - feat(archive/100-theorems-list/73_ascending_descending_sequences): Erdős–Szekeres (#3074)

mathlib
e1a72b50 - feat(archive/100-theorems-list/73_ascending_descending_sequences): Erdős–Szekeres (#3074)