We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:


Current browse context:


Change to browse by:

References & Citations


(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Mathematics > Combinatorics

Title: Formalizing Hall's Marriage Theorem in Lean

Abstract: We formalize Hall's Marriage Theorem in the Lean theorem prover for inclusion in mathlib, which is a community-driven effort to build a unified mathematics library for Lean. One goal of the mathlib project is to contain all of the topics of a complete undergraduate mathematics education.
We provide three presentations of the main theorem statement: in terms of indexed families of finite sets, of relations on types, and of matchings in bipartite graphs. We also formalize a version of K\H{o}nig's lemma (in terms of inverse limits) to boost the theorem to the case of countably infinite index sets. We give a description of the design of the recent mathlib library for simple graphs, and we also give a necessary and sufficient condition for a simple graph to carry a function.
Comments: 15 pages
Subjects: Combinatorics (math.CO); Logic in Computer Science (cs.LO)
MSC classes: 05-04 (Primary) 05C70, 68R05 (Secondary)
Cite as: arXiv:2101.00127 [math.CO]
  (or arXiv:2101.00127v1 [math.CO] for this version)

Submission history

From: Kyle Miller [view email]
[v1] Fri, 1 Jan 2021 01:10:31 GMT (36kb)

Link back to: arXiv, form interface, contact.