:: Pigeon Hole Principle
:: by Wojciech A. Trybulec
::
:: Received April 8, 1990
:: Copyright (c) 1990 Association of Mizar Users
:: deftheorem Def1 defines is_one-to-one_at FINSEQ_4:def 1 :
theorem :: FINSEQ_4:1
canceled;
theorem Th2: :: FINSEQ_4:2
theorem Th3: :: FINSEQ_4:3
theorem Th4: :: FINSEQ_4:4
theorem :: FINSEQ_4:5
:: deftheorem Def2 defines just_once_values FINSEQ_4:def 2 :
theorem :: FINSEQ_4:6
canceled;
theorem Th7: :: FINSEQ_4:7
theorem Th8: :: FINSEQ_4:8
theorem Th9: :: FINSEQ_4:9
theorem Th10: :: FINSEQ_4:10
theorem Th11: :: FINSEQ_4:11
:: deftheorem Def3 defines <- FINSEQ_4:def 3 :
theorem :: FINSEQ_4:12
canceled;
theorem :: FINSEQ_4:13
canceled;
theorem :: FINSEQ_4:14
canceled;
theorem :: FINSEQ_4:15
canceled;
theorem :: FINSEQ_4:16
theorem Th17: :: FINSEQ_4:17
theorem :: FINSEQ_4:18
theorem :: FINSEQ_4:19
canceled;
theorem :: FINSEQ_4:20
theorem :: FINSEQ_4:21
theorem :: FINSEQ_4:22
canceled;
theorem :: FINSEQ_4:23
canceled;
theorem :: FINSEQ_4:24
theorem :: FINSEQ_4:25
theorem :: FINSEQ_4:26
theorem :: FINSEQ_4:27
:: deftheorem FINSEQ_4:def 4 :
canceled;
:: deftheorem defines .. FINSEQ_4:def 5 :
theorem :: FINSEQ_4:28
canceled;
theorem Th29: :: FINSEQ_4:29
theorem Th30: :: FINSEQ_4:30
theorem Th31: :: FINSEQ_4:31
theorem Th32: :: FINSEQ_4:32
theorem Th33: :: FINSEQ_4:33
theorem Th34: :: FINSEQ_4:34
theorem Th35: :: FINSEQ_4:35
theorem Th36: :: FINSEQ_4:36
theorem Th37: :: FINSEQ_4:37
theorem Th38: :: FINSEQ_4:38
theorem :: FINSEQ_4:39
theorem Th40: :: FINSEQ_4:40
theorem Th41: :: FINSEQ_4:41
theorem :: FINSEQ_4:42
:: deftheorem Def6 defines -| FINSEQ_4:def 6 :
theorem :: FINSEQ_4:43
canceled;
theorem :: FINSEQ_4:44
canceled;
theorem Th45: :: FINSEQ_4:45
theorem Th46: :: FINSEQ_4:46
theorem Th47: :: FINSEQ_4:47
theorem Th48: :: FINSEQ_4:48
theorem Th49: :: FINSEQ_4:49
theorem :: FINSEQ_4:50
theorem :: FINSEQ_4:51
theorem :: FINSEQ_4:52
theorem :: FINSEQ_4:53
:: deftheorem Def7 defines |-- FINSEQ_4:def 7 :
theorem :: FINSEQ_4:54
canceled;
theorem :: FINSEQ_4:55
canceled;
theorem :: FINSEQ_4:56
canceled;
theorem Th57: :: FINSEQ_4:57
theorem Th58: :: FINSEQ_4:58
theorem :: FINSEQ_4:59
theorem Th60: :: FINSEQ_4:60
theorem Th61: :: FINSEQ_4:61
theorem :: FINSEQ_4:62
theorem :: FINSEQ_4:63
theorem :: FINSEQ_4:64
theorem :: FINSEQ_4:65
theorem Th66: :: FINSEQ_4:66
theorem :: FINSEQ_4:67
theorem :: FINSEQ_4:68
theorem Th69: :: FINSEQ_4:69
theorem :: FINSEQ_4:70
theorem Th71: :: FINSEQ_4:71
theorem :: FINSEQ_4:72
theorem Th73: :: FINSEQ_4:73
theorem Th74: :: FINSEQ_4:74
theorem Th75: :: FINSEQ_4:75
theorem :: FINSEQ_4:76
Lm1:
for A, B being finite set
for f being Function of A,B st card A = card B & rng f = B holds
f is one-to-one
theorem Th77: :: FINSEQ_4:77
theorem :: FINSEQ_4:78
theorem :: FINSEQ_4:79
theorem :: FINSEQ_4:80
theorem :: FINSEQ_4:81
theorem :: FINSEQ_4:82
theorem :: FINSEQ_4:83
theorem :: FINSEQ_4:84
theorem :: FINSEQ_4:85
theorem :: FINSEQ_4:86
theorem :: FINSEQ_4:87
theorem :: FINSEQ_4:88
definition
let x1,
x2,
x3,
x4 be
set ;
func <*x1,x2,x3,x4*> -> set equals :: FINSEQ_4:def 8
<*x1,x2,x3*> ^ <*x4*>;
correctness
coherence
<*x1,x2,x3*> ^ <*x4*> is set ;
;
let x5 be
set ;
func <*x1,x2,x3,x4,x5*> -> set equals :: FINSEQ_4:def 9
<*x1,x2,x3*> ^ <*x4,x5*>;
correctness
coherence
<*x1,x2,x3*> ^ <*x4,x5*> is set ;
;
end;
:: deftheorem defines <* FINSEQ_4:def 8 :
:: deftheorem defines <* FINSEQ_4:def 9 :
for
x1,
x2,
x3,
x4,
x5 being
set holds
<*x1,x2,x3,x4,x5*> = <*x1,x2,x3*> ^ <*x4,x5*>;
registration
let x1,
x2,
x3,
x4 be
set ;
cluster <*x1,x2,x3,x4*> -> Relation-like Function-like ;
coherence
( <*x1,x2,x3,x4*> is Function-like & <*x1,x2,x3,x4*> is Relation-like )
;
let x5 be
set ;
cluster <*x1,x2,x3,x4,x5*> -> Relation-like Function-like ;
coherence
( <*x1,x2,x3,x4,x5*> is Function-like & <*x1,x2,x3,x4,x5*> is Relation-like )
;
end;
registration
let x1,
x2,
x3,
x4 be
set ;
cluster <*x1,x2,x3,x4*> -> FinSequence-like ;
coherence
<*x1,x2,x3,x4*> is FinSequence-like
;
let x5 be
set ;
cluster <*x1,x2,x3,x4,x5*> -> FinSequence-like ;
coherence
<*x1,x2,x3,x4,x5*> is FinSequence-like
;
end;
definition
let D be non
empty set ;
let x1,
x2,
x3,
x4,
x5 be
Element of
D;
:: original: <*redefine func <*x1,x2,x3,x4,x5*> -> FinSequence of
D;
coherence
<*x1,x2,x3,x4,x5*> is FinSequence of D
end;
theorem Th89: :: FINSEQ_4:89
for
x1,
x2,
x3,
x4 being
set holds
(
<*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 Th90: :: FINSEQ_4:90
for
x1,
x2,
x3,
x4,
x5 being
set holds
(
<*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*> )
theorem Th91: :: FINSEQ_4:91
theorem Th92: :: FINSEQ_4:92
theorem Th93: :: FINSEQ_4:93
for
x1,
x2,
x3,
x4,
x5 being
set for
p being
FinSequence holds
(
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 ) )
theorem Th94: :: FINSEQ_4:94
theorem :: FINSEQ_4:95
for
ND being non
empty set for
y1,
y2,
y3,
y4 being
Element of
ND holds
(
<*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:96
for
ND being non
empty set for
y1,
y2,
y3,
y4,
y5 being
Element of
ND holds
(
<*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 )
theorem Th97: :: FINSEQ_4:97
theorem :: FINSEQ_4:98