在 Lean 中形式化霍尔婚配定理
组合数学
2021-01-05 v1 计算机科学中的逻辑
摘要
我们在 Lean 定理证明器中形式化了霍尔婚配定理，以纳入 mathlib，这是一个由社区驱动、为 Lean 构建统一数学库的工程。mathlib 项目的目标之一是涵盖完整本科数学教育的所有主题。我们给出定理陈述的三种形式：基于有限集的索引族、基于类型上的关系，以及基于二部图中的匹配。我们还形式化了 K\H{o}nig 引理的一个版本（以逆极限表述），以将定理推广到可数无穷索引集的情形。我们描述了近期 mathlib 简单图库的设计，并给出了简单图承载一个函数的充要条件。
引用
@article{arxiv.2101.00127,
title = {Formalizing Hall's Marriage Theorem in Lean},
author = {Alena Gusakov and Bhavik Mehta and Kyle A. Miller},
journal= {arXiv preprint arXiv:2101.00127},
year = {2021}
}
备注
15 pages