+ +
+
+ +
+
| Home | +
| About | +
| Submission | +
| Updating Entries | +
| Using Entries | +
| Search | +
| Statistics | +
| Index | +
| Download | +
+
+
+
+
+
+
+
+
+
+
+
+
+
++
The + + Nash-Williams + + Partition + + Theorem + +
++ +
| Title: | +The Nash-Williams Partition Theorem | +
| + Author: + | ++ Lawrence C. Paulson + | +
| Submission date: | +2020-05-16 | +
| Abstract: | ++In 1965, Nash-Williams discovered a generalisation of the infinite +form of Ramsey's theorem. Where the latter concerns infinite sets +of n-element sets for some fixed n, the Nash-Williams theorem concerns +infinite sets of finite sets (or lists) subject to a “no initial +segment” condition. The present formalisation follows a +monograph on Ramsey Spaces by Todorčević. | +
| BibTeX: | +
+ @article{Nash_Williams-AFP,
+ author = {Lawrence C. Paulson},
+ title = {The Nash-Williams Partition Theorem},
+ journal = {Archive of Formal Proofs},
+ month = may,
+ year = 2020,
+ note = {\url{http://isa-afp.org/entries/Nash_Williams.html},
+ Formal proof development},
+ ISSN = {2150-914x},
+}
+ |
+
| License: | +BSD License |
|
+ Proof outline + Proof document + |
+
| + Browse theories + |
| + Download this entry + | +
| Older releases: + None + |