# Formalizing Hall's Marriage Theorem in Lean

Preprint · Alena Gusakov, Bhavik Mehta, Kyle A. Miller

- Archive id: arxiv:2101.00127
- Published: 2021-01-01
- arXiv: https://arxiv.org/abs/2101.00127
- Source URL: https://arxiv.org/abs/2101.00127
- PDF: https://arxiv.org/pdf/2101.00127
- Provenance: arxiv

## 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ő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.

_Abstract reproduced under CC0-1.0 (arXiv descriptive metadata)._

---
Space Kitty Archive · https://space-kitty.com · API: https://space-kitty.com/api/v1 · MCP: https://space-kitty.com/mcp · Premium: $0.20/request via x402 (Base Sepolia (testnet)). Metadata: arXiv (CC0), OpenAlex (CC0), Europe PMC (CC BY/CC0 works), ClinicalTrials.gov.