:: Pigeon Hole Principle
:: by Wojciech A. Trybulec
::
:: Received April 8, 1990
:: Copyright (c) 1990-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, FUNCT_1, FINSEQ_1, NAT_1, RELAT_1, FINSET_1, CARD_1,
XBOOLE_0, TARSKI, XXREAL_0, SUBSET_1, PARTFUN1, ARYTM_1, ARYTM_3,
ORDINAL4, FINSEQ_4, FUNCT_2, EQREL_1, CARD_3, SETFAM_1, ZFMISC_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, ENUMSET1, SUBSET_1, ORDINAL1, RELAT_1,
CARD_1, SETFAM_1, EQREL_1, NUMBERS, XCMPLX_0, FUNCT_1, PARTFUN1, FUNCT_2,
FINSET_1, NAT_1, FINSEQ_1, FINSEQ_3, XXREAL_0;
constructors ZFMISC_1, ENUMSET1, WELLORD2, FUNCT_2, XXREAL_0, REAL_1,
PARTFUN1, NAT_1, INT_1, FINSEQ_3, RELSET_1, EQREL_1, SETFAM_1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, FINSET_1, XREAL_0, INT_1, FINSEQ_1,
ORDINAL1, CARD_1, RELSET_1, SUBSET_1, EQREL_1, NAT_1, PARTFUN1, FUNCT_2,
XXREAL_0;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
begin
reserve f for Function;
reserve p,q for FinSequence;
reserve A,B,C for set,x,x1,x2,y,z for object;
reserve k,l,m,n for Nat;
reserve a for Nat;
definition
let f; let x be object;
pred f is_one-to-one_at x means
:: FINSEQ_4:def 1
f"Im(f,x) = {x};
end;
theorem :: FINSEQ_4:1
f is_one-to-one_at x implies x in dom f;
theorem :: FINSEQ_4:2
f is_one-to-one_at x iff x in dom f & f " {f.x} = {x};
theorem :: FINSEQ_4:3
f is_one-to-one_at x iff x in dom f & for z st z in dom f & x <>
z holds f.x <> f.z;
theorem :: FINSEQ_4:4
(for x st x in dom f holds f is_one-to-one_at x) iff f is one-to-one;
definition
let R be Relation, y be object;
pred R just_once_values y means
:: FINSEQ_4:def 2
card Coim(R,y) = 1;
end;
theorem :: FINSEQ_4:5
f just_once_values y implies y in rng f;
theorem :: FINSEQ_4:6
f just_once_values y iff ex x st {x} = f " {y};
theorem :: FINSEQ_4:7
f just_once_values y iff
ex x being object st x in dom f & y = f.x &
for z being object st z in dom f & z <> x holds f.z <> y;
theorem :: FINSEQ_4:8
f is one-to-one iff for y st y in rng f holds f just_once_values y;
theorem :: FINSEQ_4:9
f is_one-to-one_at x iff x in dom f & f just_once_values f.x;
definition
let f,y;
assume
f just_once_values y;
func f <- y -> set means
:: FINSEQ_4:def 3
it in dom f & f.it = y;
end;
theorem :: FINSEQ_4:10
f just_once_values y implies Im(f, f<-y) = {y};
theorem :: FINSEQ_4:11
f just_once_values y implies f " {y} = {f <- y};
theorem :: FINSEQ_4:12
f is one-to-one & y in rng f implies (f").y = f <- y;
theorem :: FINSEQ_4:13
f is_one-to-one_at x implies f <- (f.x) = x;
theorem :: FINSEQ_4:14
f just_once_values y implies f is_one-to-one_at f <- y;
reserve D for non empty set;
reserve d,d1,d2,d3 for Element of D;
definition
let D;
let d1,d2;
redefine func <* d1,d2 *> -> FinSequence of D;
end;
definition
let D;
let d1,d2,d3;
redefine func <* d1,d2,d3 *> -> FinSequence of D;
end;
theorem :: FINSEQ_4:15
for i being Nat for D being set, P being FinSequence of D st 1 <= i &
i <= len P holds P/.i = P.i;
theorem :: FINSEQ_4:16
<* d *>/.1 = d;
theorem :: FINSEQ_4:17
<* d1,d2 *>/.1 = d1 & <* d1,d2 *>/.2 = d2;
theorem :: FINSEQ_4:18
<* d1,d2,d3 *>/.1 = d1 & <* d1,d2,d3 *>/.2 = d2 & <* d1,d2,d3 *>/.3 = d3;
definition
let p; let x be object;
func x..p -> Element of NAT equals
:: FINSEQ_4:def 4
Sgm(p " {x}).1;
end;
theorem :: FINSEQ_4:19
x in rng p implies p.(x..p) = x;
theorem :: FINSEQ_4:20
x in rng p implies x..p in dom p;
theorem :: FINSEQ_4:21
x in rng p implies 1 <= x..p & x..p <= len p;
theorem :: FINSEQ_4:22
x in rng p implies x..p - 1 is Element of NAT & len p - x..p is
Element of NAT;
theorem :: FINSEQ_4:23
x in rng p implies x..p in p " {x};
theorem :: FINSEQ_4:24
for k st k in dom p & k < x..p holds p.k <> x;
theorem :: FINSEQ_4:25
p just_once_values x implies p <- x = x..p;
theorem :: FINSEQ_4:26
p just_once_values x implies for k st k in dom p & k <> x..p holds p.k <> x;
theorem :: FINSEQ_4:27
x in rng p & (for k st k in dom p & k <> x..p holds p.k <> x)
implies p just_once_values x;
theorem :: FINSEQ_4:28
p just_once_values x iff x in rng p & {x..p} = p " {x};
theorem :: FINSEQ_4:29
p is one-to-one & x in rng p implies {x..p} = p " {x};
theorem :: FINSEQ_4:30
p just_once_values x iff len(p - {x}) = len p - 1;
reserve L,M for Element of NAT;
theorem :: FINSEQ_4:31
p just_once_values x implies for k st k in dom(p - {x}) holds (k
< x..p implies (p - {x}).k = p.k) & (x..p <= k implies (p - {x}).k = p.(k + 1))
;
theorem :: FINSEQ_4:32
p is one-to-one & x in rng p implies for k st k in dom(p - {x}) holds
((p - {x}).k = p.k iff k < x..p) & ((p - {x}).k = p.(k + 1) iff x..p <= k);
definition
let p;
let x;
assume
x in rng p;
func p -| x -> FinSequence means
:: FINSEQ_4:def 5
ex n st n = x..p - 1 & it = p | Seg n;
end;
theorem :: FINSEQ_4:33
x in rng p & n = x..p - 1 implies p | Seg n = p -| x;
theorem :: FINSEQ_4:34
x in rng p implies len(p -| x) = x..p - 1;
theorem :: FINSEQ_4:35
x in rng p & n = x..p - 1 implies dom(p -| x) = Seg n;
theorem :: FINSEQ_4:36
x in rng p & k in dom(p -| x) implies p.k = (p -| x).k;
theorem :: FINSEQ_4:37
x in rng p implies not x in rng(p -| x);
theorem :: FINSEQ_4:38
x in rng p implies rng(p -| x) misses {x};
theorem :: FINSEQ_4:39
x in rng p implies rng(p -| x) c= rng p;
theorem :: FINSEQ_4:40
x in rng p implies (x..p = 1 iff p -| x = {});
theorem :: FINSEQ_4:41
x in rng p & p is FinSequence of D implies p -| x is FinSequence of D;
definition
let p;
let x;
assume
x in rng p;
func p |-- x -> FinSequence means
:: FINSEQ_4:def 6
len it = len p - x..p & for k st k in dom it holds it.k = p.(k + x..p);
end;
theorem :: FINSEQ_4:42
x in rng p & n = len p - x..p implies dom(p |-- x) = Seg n;
theorem :: FINSEQ_4:43
x in rng p & n in dom(p |-- x) implies n + x..p in dom p;
theorem :: FINSEQ_4:44
x in rng p implies rng(p |-- x) c= rng p;
theorem :: FINSEQ_4:45
p just_once_values x iff x in rng p & not x in rng(p |-- x);
theorem :: FINSEQ_4:46
x in rng p & p is one-to-one implies not x in rng(p |-- x);
theorem :: FINSEQ_4:47
p just_once_values x iff x in rng p & rng(p |-- x) misses {x};
theorem :: FINSEQ_4:48
x in rng p & p is one-to-one implies rng(p |-- x) misses {x};
theorem :: FINSEQ_4:49
x in rng p implies (x..p = len p iff p |-- x = {});
theorem :: FINSEQ_4:50
x in rng p & p is FinSequence of D implies p |-- x is FinSequence of D;
theorem :: FINSEQ_4:51
x in rng p implies p = (p -| x) ^ <* x *> ^ (p |-- x);
theorem :: FINSEQ_4:52
x in rng p & p is one-to-one implies p -| x is one-to-one;
theorem :: FINSEQ_4:53
x in rng p & p is one-to-one implies p |-- x is one-to-one;
theorem :: FINSEQ_4:54
p just_once_values x iff x in rng p & p - {x} = (p -| x) ^ (p |-- x);
theorem :: FINSEQ_4:55
x in rng p & p is one-to-one implies p - {x} = (p -| x) ^ (p |-- x);
theorem :: FINSEQ_4:56
x in rng p & p - {x} is one-to-one & p - {x} = (p -| x) ^ (p |--
x) implies p is one-to-one;
theorem :: FINSEQ_4:57
x in rng p & p is one-to-one implies rng(p -| x) misses rng(p |-- x);
theorem :: FINSEQ_4:58
A is finite implies ex p st rng p = A & p is one-to-one;
theorem :: FINSEQ_4:59
rng p c= dom p & p is one-to-one implies rng p = dom p;
theorem :: FINSEQ_4:60
rng p = dom p implies p is one-to-one;
theorem :: FINSEQ_4:61
rng p = rng q & len p = len q & q is one-to-one implies p is one-to-one;
theorem :: FINSEQ_4:62
p is one-to-one iff card rng p = len p;
:: If you are looking for theorem
:: rng p = rng q & p is one-to-one & q is one-to-one implies len p = len q,
:: it is placed in RLVECT_1 under number 106.
reserve f for Function of A,B;
theorem :: FINSEQ_4:63
for A,B being finite set, f being Function of A,B st
card A = card B holds f is one-to-one iff f is onto;
::$CT
::$N Dirichlet Principle
::$N Pigeon Hole Principle
theorem :: FINSEQ_4:65
card B in card A & B <> {} implies ex x,y st x in A & y in A & x <> y
& f.x = f.y;
theorem :: FINSEQ_4:66
card A in card B implies ex x st x in B & for y st y in A holds f.y <> x;
begin :: Addenda
:: from TOPREAL4
theorem :: FINSEQ_4:67
for D being non empty set, f being FinSequence of D,
p being Element of D holds (f^<*p*>)/.(len f + 1) = p;
:: from GROUP_5
theorem :: FINSEQ_4:68
for E being non empty set, p,q being FinSequence of E st k in dom p
holds (p ^ q)/.k = p/.k;
theorem :: FINSEQ_4:69
for E being non empty set, p,q being FinSequence of E st k in dom q
holds (p ^ q)/.(len p + k) = q/.k;
:: from TOPREAL1
theorem :: FINSEQ_4:70
for m being Nat for D being set, p being FinSequence of D st
a in dom(p|m) holds (p|m qua FinSequence of D)/.a = p/.a;
:: from GOBOARD1
theorem :: FINSEQ_4:71
for D being set, f being FinSequence of D, n,m st n in dom f & m in
Seg n holds m in dom f & (f|n)/.m = f/.m;
:: from VECTSP_9, 2006.01.06, A.T.
theorem :: FINSEQ_4:72
for X being finite set st n <= card X holds ex A being finite Subset
of X st card A = n;
reserve f for Function;
theorem :: FINSEQ_4:73
f is one-to-one & x in rng f implies card Coim (f,x) = 1;
:: form SCMPDS_1, 2006.03.24, A.T.
definition
let x1,x2,x3,x4 be object;
func <*x1,x2,x3,x4*> -> set equals
:: FINSEQ_4:def 7
<*x1,x2,x3*>^<*x4*>;
let x5 be object;
func <*x1,x2,x3,x4,x5*> -> set equals
:: FINSEQ_4:def 8
<*x1,x2,x3*>^<*x4,x5*>;
end;
registration
let x1,x2,x3,x4 be object;
cluster <*x1,x2,x3,x4*> -> non empty Function-like Relation-like;
let x5 be object;
cluster <*x1,x2,x3,x4,x5*> -> non empty Function-like Relation-like;
end;
registration
let x1,x2,x3,x4 be object;
cluster <*x1,x2,x3,x4*> -> FinSequence-like;
let x5 be object;
cluster <*x1,x2,x3,x4,x5*> -> FinSequence-like;
end;
definition
let D be non empty set,x1,x2,x3,x4 be Element of D;
redefine func <* x1,x2,x3,x4*> -> FinSequence of D;
end;
definition
let D be non empty set,x1,x2,x3,x4,x5 be Element of D;
redefine func <*x1,x2,x3,x4,x5*> -> FinSequence of D;
end;
reserve x1,x2,x3,x4,x5 for object;
theorem :: FINSEQ_4:74
<*x1,x2,x3,x4*>=<*x1,x2,x3*>^<*x4*> & <*x1,x2,x3,x4*>=<*x1,x2*>^
<*x3,x4*> & <*x1,x2,x3,x4*>=<*x1*>^<*x2,x3,x4*> & <*x1,x2,x3,x4*>=<*x1*>^<*x2*>
^<*x3*>^<*x4*>;
theorem :: FINSEQ_4:75
<*x1,x2,x3,x4,x5*>=<*x1,x2,x3*>^<*x4,x5*> & <*x1,x2,x3,x4,x5*>=
<*x1,x2,x3,x4*>^<*x5*> & <*x1,x2,x3,x4,x5*>=<*x1*>^<*x2*>^<*x3*>^<*x4*>^<*x5*>
& <*x1,x2,x3,x4,x5*>=<*x1,x2*>^<*x3,x4,x5*> & <*x1,x2,x3,x4,x5*>=<*x1*>^<*x2,x3
,x4,x5*>;
reserve p for FinSequence;
theorem :: FINSEQ_4:76
p = <*x1,x2,x3,x4*> iff len p = 4 & p.1 = x1 & p.2 = x2 & p.3=x3 & p.4= x4;
::$CT
theorem :: FINSEQ_4:78
p = <*x1,x2,x3,x4,x5*> iff len p = 5 & p.1 = x1 & p.2 = x2 & p.3
=x3 & p.4= x4 & p.5= x5;
reserve ND for non empty set;
reserve y1,y2,y3,y4,y5 for Element of ND;
::$CT
theorem :: FINSEQ_4:80
<*y1,y2,y3,y4*>/.1 = y1 & <*y1,y2,y3,y4*>/.2 = y2 & <*y1,y2,y3,y4*>/.3
= y3 & <*y1,y2,y3,y4*>/.4=y4;
theorem :: FINSEQ_4:81
<*y1,y2,y3,y4,y5*>/.1 = y1 & <*y1,y2,y3,y4,y5*>/.2 = y2 & <*y1,y2,y3,
y4,y5*>/.3 = y3 & <*y1,y2,y3,y4,y5*>/.4=y4 & <*y1,y2,y3,y4,y5*>/.5=y5;
:: form GOBOARD1, 2007.07.22, A.T.
scheme :: FINSEQ_4:sch 1
Sch1{D()->non empty set, N()->Nat, P[object,object]}:
ex f being FinSequence of D(
) st len f = N() & for n st n in Seg N() holds P[n,f/.n]
provided
for n st n in Seg N() ex d being Element of D() st P[n,d];
:: form SCMFSA_7, 2007.07.22, A.T.
theorem :: FINSEQ_4:82
for D being non empty set, p,q being FinSequence of D st p c= q
holds ex p9 being FinSequence of D st p ^ p9 = q;
theorem :: FINSEQ_4:83
for D being non empty set, p,q being FinSequence of D, i being Element
of NAT st p c= q & 1 <= i & i <= len p holds q.i = p.i;
:: form GOBOARD2, 2008.03.08, A.T.
scheme :: FINSEQ_4:sch 2
PiLambdaD{D()-> non empty set, l()->Nat, F(set)-> Element of D()}: ex g
being FinSequence of D() st len g=l() & for n being Nat st n in dom g holds g/.
n=F(n);
:: from CIRCCMB3, 2009.02.16, A.T.
registration
let x1,x2,x3,x4 be object;
cluster <*x1,x2,x3,x4*> -> 4-element;
let x5 be object;
cluster <*x1,x2,x3,x4,x5*> -> 5-element;
end;
begin :: Moved from FSM_1, 2010.03.16, A.T.
theorem :: FINSEQ_4:84
for m, n being Nat holds m < n implies ex p being Element of NAT
st n = m+p & 1 <= p;
theorem :: FINSEQ_4:85
for S being set, D1, D2 being non empty set, f1 being Function of
S, D1, f2 being Function of D1, D2 holds f1 is bijective & f2 is bijective
implies f2*f1 is bijective;
:: Partitions & Equivalence Relations
theorem :: FINSEQ_4:86
for Y being set, E1, E2 being Equivalence_Relation of Y st
Class E1 = Class E2 holds E1 = E2;
registration
let Z be finite set;
cluster -> finite for a_partition of Z;
end;
registration
let X be non empty finite set;
cluster non empty finite for a_partition of X;
end;
theorem :: FINSEQ_4:87
for X being non empty set, PX being a_partition of X
for Pi being set st Pi in PX ex x being Element of X st x in Pi;
reserve X, A for non empty finite set,
PX for a_partition of X,
PA1, PA2 for a_partition of A;
theorem :: FINSEQ_4:88
card PX <= card X;
theorem :: FINSEQ_4:89
PA1 is_finer_than PA2 implies card PA2 <= card PA1;
theorem :: FINSEQ_4:90
PA1 is_finer_than PA2 implies for p2 being Element of PA2
ex p1 being Element of PA1 st p1 c= p2;
theorem :: FINSEQ_4:91
PA1 is_finer_than PA2 & card PA1 = card PA2 implies PA1 = PA2;
registration
let D be set, M be FinSequence of D*;
let k;
cluster M/.k -> Function-like Relation-like;
:: pewnie wystarczy 'D*-valued'
end;
registration
let D be set, M be FinSequence of D*;
let k;
cluster M/.k -> FinSequence-like D-valued for Function;
end;
reserve f for FinSequence of D;
theorem :: FINSEQ_4:92
m in dom f implies f/.1 = (f|m)/.1;
theorem :: FINSEQ_4:93
m in dom f implies f/.m = (f|m)/.len(f|m);