|
|
|
|
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
infinite_pigeonhole.pvs
Sprache: PVS
Original von: PVS©
|
|
% proof that a function from an infinite domain to a finite range
% has an infinite mono-chromatic subdomain
%
% Author: Alfons Geser ([email protected]), 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.15 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
|
|
|
|
|
