| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/orders/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 756 B |
|
Quelle infinite_pigeonhole.pvs Sprache: PVS |
|||||||||
|
% proof that a function from an infinite domain to a finite range
% has an infinite mono-chromatic subdomain % % Author: Alfons Geser (geser@nianet.org), National Institute of Aerospace % Date: Dec 2004 infinite_pigeonhole[D, R: TYPE]: THEORY BEGIN ASSUMING domain_infiniteness: ASSUMPTION NOT is_finite_type[D] range_finiteness: ASSUMPTION is_finite_type[R] ENDASSUMING CONVERSION+ singleton d: VAR D r: VAR R f: VAR [D -> R] % the domain of a function can be represented as the disjoint union of % the inverse images of every range element Union_inverse_image: LEMMA FORALL f: fullset[D] = IUnion[R, D](inverse_image(f)) infinite_pigeonhole: LEMMA EXISTS r: is_infinite(inverse_image(f, r)) END infinite_pigeonhole ¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28