:: 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);