Hall's theorem for enumerable families of finite sets

DOI10.1007/978-3-031-16681-5_7OpenAlexW4296118851MaRDI QIDQ6159371

Mauricio Ayala-Rincón, Thaynara Arielly de Lima, Fabián Fernando Serrano Suárez

Publication date: 2 June 2023

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-031-16681-5_7

zbMATH Keywords

compactness theoremIsabelle/HOLHall's theoremformalisation

Mathematics Subject Classification ID

Computer science support for mathematical research and practice (68Vxx)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear quantifier elimination
• A formal proof of the minor-exclusion property for treewidth-two graphs
• Graph theory in Coq: minors, treewidth, and isomorphisms
• Towards a constructive formalization of perfect graph theorems
• Proof Pearl: The Marriage Theorem
• Proofs from THE BOOK
• On Representatives of Subsets
• Note on the Transfinite Case of Hall's Theorem on Representatives
• The Marriage Problem

This page was built for publication: Hall's theorem for enumerable families of finite sets