arXiv · math/9405204
An Induction Principle and Pigeonhole Principles for K-Finite Sets
Abstract
We establish a course-of-values induction principle for K-finite sets in intuitionistic type theory. Using this principle, we prove a pigeonhole principle conjectured by Benabou and Loiseau. We also comment on some variants of this pigeonhole principle.
Explore related subjects
Keep this discovery
Andreas Blass. 1994-05-20. An Induction Principle and Pigeonhole Principles for K-Finite Sets. https://arxiv.org/abs/math/9405204
Cite the original work for its findings. Save a collection to share your selection of sources.