:: STIRL2_1 semantic presentation

definition

let k be Nat;
:: original: {
redefine func {k} -> Subset of NAT ;
coherence by SUBSET_1:55;
let l be Nat;
:: original: {
redefine func {k,l} -> Subset of NAT ;
coherence by SUBSET_1:56;
let m be Nat;
:: original: {
redefine func {k,l,m} -> non empty Subset of NAT ;
coherence by SUBSET_1:57, ENUMSET1:def 1;

end;

theorem Th1: :: STIRL2_1:1

for N being non empty Subset of NAT holds min N = min* N

proof end;

theorem Th2: :: STIRL2_1:2

for K, N being non empty Subset of NAT holds min (min K),(min N) = min (K \/ N)

proof end;

theorem :: STIRL2_1:3

for Ke, Ne being Subset of NAT holds min (min* Ke),(min* Ne) <= min* (Ke \/ Ne)

proof end;

theorem :: STIRL2_1:4

for Ne, Ke being Subset of NAT st not min* Ne in Ne /\ Ke holds
min* Ne = min* (Ne \ Ke)

proof end;

theorem Th5: :: STIRL2_1:5

for n being Nat holds
( min* {n} = n & min {n} = n )

proof end;

theorem Th6: :: STIRL2_1:6

for n, k being Nat holds
( min* {n,k} = min n,k & min {n,k} = min n,k )

proof end;

theorem :: STIRL2_1:7

for n, k, l being Nat holds min* {n,k,l} = min n,(min k,l)

proof end;

theorem Th8: :: STIRL2_1:8

for n being Nat holds n is Subset of NAT

proof end;

registration

let n be Nat;
cluster -> natural Element of n;
coherence

proof end;

end;

theorem :: STIRL2_1:9

for n being Nat
for N being non empty Subset of NAT st N c= n holds
n - 1 is Nat

proof end;

theorem Th10: :: STIRL2_1:10

for k, n being Nat st k in n holds
( k <= n - 1 & n - 1 is Nat )

proof end;

theorem :: STIRL2_1:11

for n being Nat holds min* n = 0

proof end;

theorem Th12: :: STIRL2_1:12

for n being Nat
for N being non empty Subset of NAT st N c= n holds
min* N <= n - 1

proof end;

theorem :: STIRL2_1:13

for n being Nat
for N being non empty Subset of NAT st N c= n & N <> {(n - 1)} holds
min* N < n - 1

proof end;

theorem Th14: :: STIRL2_1:14

for n being Nat
for Ne being Subset of NAT st Ne c= n & n > 0 holds
min* Ne <= n - 1

proof end;

definition

let n be Nat;
let X be set ;
let f be Function of n,X;
let x be set ;
:: original: "
redefine func f " x -> Subset of NAT ;
coherence

proof end;

end;

definition

let X be set ;
let k be Nat;
let f be Function of X,k;
let x be set ;
:: original: .
redefine func f . x -> Element of k;
coherence

proof end;

end;

registration

let X be set ;
let Ne be Subset of NAT ;
let f be Function of X,Ne;
let x be set ;
cluster f . x -> natural ;
coherence

proof end;

end;

definition

let n, k be Nat;
let f be Function of n,k;
attr f is "increasing means :Def1: :: STIRL2_1:def 1
( ( n = 0 implies k = 0 ) & ( k = 0 implies n = 0 ) & ( for l, m being Nat st l in rng f & m in rng f & l < m holds
min* (f " {l}) < min* (f " {m}) ) );

end;

:: deftheorem Def1 defines "increasing STIRL2_1:def 1 :

theorem Th15: :: STIRL2_1:15

for n, k being Nat
for f being Function of n,k st n = 0 & k = 0 holds
( f is onto & f is "increasing )

proof end;

theorem Th16: :: STIRL2_1:16

for k, n, m being Nat
for f being Function of n,k st n > 0 holds
min* (f " {m}) <= n - 1

proof end;

theorem Th17: :: STIRL2_1:17

for n, k being Nat
for f being Function of n,k st f is onto holds
n >= k

proof end;

theorem Th18: :: STIRL2_1:18

for n, k being Nat
for f being Function of n,k st f is onto & f is "increasing holds
for m being Nat st m < k holds
m <= min* (f " {m})

proof end;

theorem Th19: :: STIRL2_1:19

for k, n being Nat
for f being Function of n,k st f is onto & f is "increasing holds
for m being Nat st m < k holds
min* (f " {m}) <= (n - k) + m

proof end;

theorem Th20: :: STIRL2_1:20

for n, k being Nat
for f being Function of n,k st f is onto & f is "increasing & n = k holds
f = id n

proof end;

theorem :: STIRL2_1:21

for k, n being Nat
for f being Function of n,k st f = id n & n > 0 holds
f is "increasing

proof end;

theorem :: STIRL2_1:22

for n, k being Nat holds
not ( ( n = 0 implies k = 0 ) & ( k = 0 implies n = 0 ) & ( for f being Function of n,k holds not f is "increasing ) )

proof end;

theorem Th23: :: STIRL2_1:23

for n, k being Nat holds
not ( ( n = 0 implies k = 0 ) & ( k = 0 implies n = 0 ) & n >= k & ( for f being Function of n,k holds
( not f is onto or not f is "increasing ) ) )

proof end;

scheme :: STIRL2_1:sch 1
Sch1{ F₁() -> Nat, F₂() -> Nat, P₁[ set ] } :

{ f where f is Function of F₁(),F₂() : P₁[f] } is finite

proof end;

theorem Th24: :: STIRL2_1:24

for n, k being Nat holds { f where f is Function of n,k : ( f is onto & f is "increasing ) } is finite

proof end;

theorem Th25: :: STIRL2_1:25

for n, k being Nat holds Card { f where f is Function of n,k : ( f is onto & f is "increasing ) } is Nat

proof end;

definition

let n, k be Nat;
func n block k -> Nat equals :: STIRL2_1:def 2
Card { f where f is Function of n,k : ( f is onto & f is "increasing ) } ;
coherence by Th25;

end;

:: deftheorem defines block STIRL2_1:def 2 :

theorem Th26: :: STIRL2_1:26

for n being Nat holds n block n = one

proof end;

theorem Th27: :: STIRL2_1:27

for k being Nat st k <> 0 holds
0 block k = 0

proof end;

theorem :: STIRL2_1:28

for k being Nat holds
( 0 block k = one iff k = 0 ) by Th26, Th27;

theorem Th29: :: STIRL2_1:29

for n, k being Nat st n < k holds
n block k = 0

proof end;

theorem :: STIRL2_1:30

for n being Nat holds
( n block 0 = one iff n = 0 )

proof end;

theorem Th31: :: STIRL2_1:31

for n being Nat st n <> 0 holds
n block 0 = 0

proof end;

theorem Th32: :: STIRL2_1:32

for n being Nat st n <> 0 holds
n block 1 = one

proof end;

Lm1: for X being set holds
( Card X = 0 iff X is empty )
by CARD_2:59, CARD_1:47;

theorem :: STIRL2_1:33

for k, n being Nat holds
( ( ( 1 <= k & k <= n ) or k = n ) iff n block k > 0 )

proof end;

scheme :: STIRL2_1:sch 2
Sch2{ F₁() -> set , F₂() -> set , F₃() -> set , F₄() -> set , F₅() -> Function of F₁(),F₂(), F₆( set ) -> set } :

ex h being Function of F₃(),F₄() st
( h | F₁() = F₅() & ( for x being set st x in F₃() \ F₁() holds
h . x = F₆(x) ) )

provided

A1: for x being set st x in F₃() \ F₁() holds
F₆(x) in F₄() and
A2: ( F₁() c= F₃() & F₂() c= F₄() ) and
A3: ( F₂() is empty implies F₁() is empty )

proof end;

scheme :: STIRL2_1:sch 3
Sch3{ F₁() -> set , F₂() -> set , F₃() -> set , F₄() -> set , F₅( set ) -> set , P₁[ set , set , set ] } :

Card { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } = Card { f where f is Function of F₃(),F₄() : ( P₁[f,F₃(),F₄()] & rng (f | F₁()) c= F₂() & ( for x being set st x in F₃() \ F₁() holds
f . x = F₅(x) ) ) }

provided

A1: for x being set st x in F₃() \ F₁() holds
F₅(x) in F₄() and
A2: ( F₁() c= F₃() & F₂() c= F₄() ) and
A3: ( F₂() is empty implies F₁() is empty ) and
A4: for f being Function of F₃(),F₄() st ( for x being set st x in F₃() \ F₁() holds
F₅(x) = f . x ) holds
( P₁[f,F₃(),F₄()] iff P₁[f | F₁(),F₁(),F₂()] )

proof end;

scheme :: STIRL2_1:sch 4
Sch4{ F₁() -> set , F₂() -> set , F₃() -> set , F₄() -> set , P₁[ set , set , set ] } :

Card { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } = Card { f where f is Function of F₁() \/ {F₃()},F₂() \/ {F₄()} : ( P₁[f,F₁() \/ {F₃()},F₂() \/ {F₄()}] & rng (f | F₁()) c= F₂() & f . F₃() = F₄() ) }

provided

A1: ( F₂() is empty implies F₁() is empty ) and
A2: not F₃() in F₁() and
A3: for f being Function of F₁() \/ {F₃()},F₂() \/ {F₄()} st f . F₃() = F₄() holds
( P₁[f,F₁() \/ {F₃()},F₂() \/ {F₄()}] iff P₁[f | F₁(),F₁(),F₂()] )

proof end;

theorem Th34: :: STIRL2_1:34

for n, k being Nat
for f being Function of n + 1,k + 1 st f is onto & f is "increasing & f " {(f . n)} = {n} holds
f . n = k

proof end;

theorem Th35: :: STIRL2_1:35

for n, k being Nat
for f being Function of n + 1,k st k <> 0 & f " {(f . n)} <> {n} holds
ex m being Nat st
( m in f " {(f . n)} & m <> n )

proof end;

theorem Th36: :: STIRL2_1:36

for n, k, m, l being Nat
for f being Function of n,k
for g being Function of n + m,k + l st g is "increasing & f = g | n holds
for i, j being Nat st i in rng f & j in rng f & i < j holds
min* (f " {i}) < min* (f " {j})

proof end;

theorem Th37: :: STIRL2_1:37

for n, k being Nat
for f being Function of n + 1,k + 1 st f is onto & f is "increasing & f " {(f . n)} = {n} holds
( rng (f | n) c= k & ( for g being Function of n,k st g = f | n holds
( g is onto & g is "increasing ) ) )

proof end;

theorem Th38: :: STIRL2_1:38

for n, k being Nat
for f being Function of n + 1,k
for g being Function of n,k st f is onto & f is "increasing & f " {(f . n)} <> {n} & f | n = g holds
( g is onto & g is "increasing )

proof end;

theorem Th39: :: STIRL2_1:39

for n, k, m being Nat
for f being Function of n,k
for g being Function of n + 1,k + m st f is onto & f is "increasing & f = g | n holds
for i, j being Nat st i in rng g & j in rng g & i < j holds
min* (g " {i}) < min* (g " {j})

proof end;

theorem Th40: :: STIRL2_1:40

for n, k being Nat
for f being Function of n,k
for g being Function of n + 1,k + 1 st f is onto & f is "increasing & f = g | n & g . n = k holds
( g is onto & g is "increasing & g " {(g . n)} = {n} )

proof end;

theorem Th41: :: STIRL2_1:41

for n, k being Nat
for f being Function of n,k
for g being Function of n + 1,k st f is onto & f is "increasing & f = g | n & g . n < k holds
( g is onto & g is "increasing & g " {(g . n)} <> {n} )

proof end;

Lm2: for n being Nat holds n + 1 = n \/ {n}
by AFINSQ_1:4;

Lm3: for k, n being Nat st k < n holds
n \/ {k} = n

proof end;

theorem Th42: :: STIRL2_1:42

for n, k being Nat holds Card { f where f is Function of n + 1,k + 1 : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } = Card { f where f is Function of n,k : ( f is onto & f is "increasing ) }

proof end;

theorem Th43: :: STIRL2_1:43

for k, n, l being Nat st l < k holds
Card { f where f is Function of n + 1,k : ( f is onto & f is "increasing & f " {(f . n)} <> {n} & f . n = l ) } = Card { f where f is Function of n,k : ( f is onto & f is "increasing ) }

proof end;

definition

let D be non empty set ;
let F be XFinSequence of D;
let b be BinOp of D;
assume A1: ( b has_a_unity or len F >= 1 ) ;
func b "**" F -> Element of D means :Def3: :: STIRL2_1:def 3
it = the_unity_wrt b if ( b has_a_unity & len F = 0 )
otherwise ex f being Function of NAT ,D st
( f . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds
f . (n + 1) = b . (f . n),(F . (n + 1)) ) & it = f . ((len F) - 1) );
existence

proof end;

uniqueness

proof end;

consistency ;

end;

:: deftheorem Def3 defines "**" STIRL2_1:def 3 :

theorem Th44: :: STIRL2_1:44

for D being non empty set
for b being BinOp of D
for d being Element of D holds b "**" <%d%> = d

proof end;

theorem Th45: :: STIRL2_1:45

for D being non empty set
for F being XFinSequence of D
for b being BinOp of D
for d being Element of D st ( b has_a_unity or len F > 0 ) holds
b "**" (F ^ <%d%>) = b . (b "**" F),d

proof end;

theorem Th46: :: STIRL2_1:46

for D being non empty set
for F being XFinSequence of D st F <> <%> D holds
ex G being XFinSequence of D ex d being Element of D st F = G ^ <%d%>

proof end;

scheme :: STIRL2_1:sch 5
Sch5{ F₁() -> non empty set , P₁[ set ] } :

for F being XFinSequence of F₁() holds P₁[F]

provided

A1: P₁[ <%> F₁()] and
A2: for F being XFinSequence of F₁()
for d being Element of F₁() st P₁[F] holds
P₁[F ^ <%d%>]

proof end;

theorem :: STIRL2_1:47

for D being non empty set
for F, G being XFinSequence of D
for b being BinOp of D st b is associative & ( b has_a_unity or ( len F >= 1 & len G >= 1 ) ) holds
b "**" (F ^ G) = b . (b "**" F),(b "**" G)

proof end;

definition

let D be non empty set ;
let d, d1 be Element of D;
:: original: <%
redefine func <%d,d1%> -> XFinSequence of D;
coherence

proof end;

let d2 be Element of D;
:: original: <%
redefine func <%d,d1,d2%> -> XFinSequence of D;
coherence

proof end;

end;

theorem :: STIRL2_1:48

for D being non empty set
for b being BinOp of D
for d1, d2 being Element of D holds b "**" <%d1,d2%> = b . d1,d2

proof end;

theorem :: STIRL2_1:49

for D being non empty set
for b being BinOp of D
for d, d1, d2 being Element of D holds b "**" <%d,d1,d2%> = b . (b . d,d1),d2

proof end;

definition

let Fn be XFinSequence of NAT ;
func Sum Fn -> Nat equals :: STIRL2_1:def 4
addnat "**" Fn;
coherence ;

end;

:: deftheorem defines Sum STIRL2_1:def 4 :

definition

let Fn be XFinSequence of NAT ;
let x be set ;
:: original: .
redefine func Fn . x -> Nat;
coherence

proof end;

end;

theorem Th50: :: STIRL2_1:50

for k being Nat
for Fn being XFinSequence of NAT st ( for n being Nat st n in dom Fn holds
Fn . n <= k ) holds
Sum Fn <= (len Fn) * k

proof end;

theorem Th51: :: STIRL2_1:51

for k being Nat
for Fn being XFinSequence of NAT st ( for n being Nat st n in dom Fn holds
Fn . n >= k ) holds
Sum Fn >= (len Fn) * k

proof end;

theorem Th52: :: STIRL2_1:52

for k being Nat
for Fn being XFinSequence of NAT st len Fn > 0 & ex x being set st
( x in dom Fn & Fn . x = k ) holds
Sum Fn >= k

proof end;

theorem :: STIRL2_1:53

for Fn being XFinSequence of NAT holds
( Sum Fn = 0 iff ( len Fn = 0 or for n being Nat st n in dom Fn holds
Fn . n = 0 ) )

proof end;

theorem Th54: :: STIRL2_1:54

for f being Function
for n being Nat holds (union (rng (f | n))) \/ (f . n) = union (rng (f | (n + 1)))

proof end;

scheme :: STIRL2_1:sch 6
Sch6{ F₁() -> non empty set , F₂() -> Nat, P₁[ set , set ] } :

ex p being XFinSequence of F₁() st
( dom p = F₂() & ( for k being Nat st k in F₂() holds
P₁[k,p . k] ) )

provided

A1: for k being Nat st k in F₂() holds
ex x being Element of F₁() st P₁[k,x]

proof end;

scheme :: STIRL2_1:sch 7
Sch7{ F₁() -> non empty set , F₂() -> XFinSequence of F₁() } :

ex CardF being XFinSequence of NAT st
( dom CardF = dom F₂() & ( for i being Nat st i in dom CardF holds
CardF . i = Card (F₂() . i) ) & Card (union (rng F₂())) = Sum CardF )

provided

A1: for i being Nat st i in dom F₂() holds
F₂() . i is finite and
A2: for i, j being Nat st i in dom F₂() & j in dom F₂() & i <> j holds
F₂() . i misses F₂() . j

proof end;

scheme :: STIRL2_1:sch 8
Sch8{ F₁() -> finite set , F₂() -> finite set , F₃() -> set , P₁[ set ], F₄() -> Function of card F₂(),F₂() } :

ex F being XFinSequence of NAT st
( dom F = card F₂() & Card { g where g is Function of F₁(),F₂() : P₁[g] } = Sum F & ( for i being Nat st i in dom F holds
F . i = Card { g where g is Function of F₁(),F₂() : ( P₁[g] & g . F₃() = F₄() . i ) } ) )

provided

A1: ( F₄() is onto & F₄() is one-to-one ) and
A2: not F₂() is empty and
A3: F₃() in F₁()

proof end;

theorem Th55: :: STIRL2_1:55

for k, n being Nat holds k * (n block k) = Card { f where f is Function of n + 1,k : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) }

proof end;

theorem Th56: :: STIRL2_1:56

for n, k being Nat holds (n + 1) block (k + 1) = ((k + 1) * (n block (k + 1))) + (n block k)

proof end;

theorem Th57: :: STIRL2_1:57

for n being Nat st n >= 1 holds
n block 2 = (1 / 2) * ((2 |^ n) - 2)

proof end;

theorem Th58: :: STIRL2_1:58

for n being Nat st n >= 2 holds
n block 3 = (1 / 6) * (((3 |^ n) - (3 * (2 |^ n))) + 3)

proof end;

Lm4: for n being Nat holds n |^ 3 = (n * n) * n

proof end;

theorem :: STIRL2_1:59

for n being Nat st n >= 3 holds
n block 4 = (1 / 24) * ((((4 |^ n) - (4 * (3 |^ n))) + (6 * (2 |^ n))) - 4)

proof end;

theorem Th60: :: STIRL2_1:60

( 3 ! = 6 & 4 ! = 24 )

proof end;

theorem Th61: :: STIRL2_1:61

for n being Nat holds
( n choose 1 = n & n choose 2 = (n * (n - 1)) / 2 & n choose 3 = ((n * (n - 1)) * (n - 2)) / 6 & n choose 4 = (((n * (n - 1)) * (n - 2)) * (n - 3)) / 24 )

proof end;

theorem Th62: :: STIRL2_1:62

for n being Nat holds (n + 1) block n = (n + 1) choose 2

proof end;

theorem :: STIRL2_1:63

for n being Nat holds (n + 2) block n = (3 * ((n + 2) choose 4)) + ((n + 2) choose 3)

proof end;

theorem Th64: :: STIRL2_1:64

for F being Function
for y being set holds
( rng (F | ((dom F) \ (F " {y}))) = (rng F) \ {y} & ( for x being set st x <> y holds
(F | ((dom F) \ (F " {y}))) " {x} = F " {x} ) )

proof end;

theorem Th65: :: STIRL2_1:65

for k being Nat
for X, x being set st Card X = k + 1 & x in X holds
Card (X \ {x}) = k

proof end;

scheme :: STIRL2_1:sch 9
Sch9{ P₁[ set ], P₂[ set , Function] } :

for F being Function st rng F is finite holds
P₁[F]

provided

A1: P₁[ {} ] and
A2: for F being Function st ( for x being set st x in rng F & P₂[x,F] holds
P₁[F | ((dom F) \ (F " {x}))] ) holds
P₁[F]

proof end;

theorem Th66: :: STIRL2_1:66

for N being Subset of NAT st N is finite holds
ex k being Nat st
for n being Nat st n in N holds
n <= k

proof end;

theorem Th67: :: STIRL2_1:67

for X, Y, x, y being set st ( Y is empty implies X is empty ) & not x in X holds
for F being Function of X,Y ex G being Function of X \/ {x},Y \/ {y} st
( G | X = F & G . x = y )

proof end;

theorem Th68: :: STIRL2_1:68

for X, Y, x, y being set st ( Y is empty implies X is empty ) holds
for F being Function of X,Y
for G being Function of X \/ {x},Y \/ {y} st G | X = F & G . x = y holds
( ( F is onto implies G is onto ) & ( not y in Y & F is one-to-one implies G is one-to-one ) )

proof end;

Lm5: for X, x being set st x in X holds
(X \ {x}) \/ {x} = X
by ZFMISC_1:140;

theorem Th69: :: STIRL2_1:69

for N being finite Subset of NAT ex Order being Function of N, card N st
( Order is bijective & ( for n, k being Nat st n in dom Order & k in dom Order & n < k holds
Order . n < Order . k ) )

proof end;

Lm6: for X being finite set
for x being set st x in X holds
card (X \ {x}) < card X

proof end;

theorem Th70: :: STIRL2_1:70

for X, Y being finite set
for F being Function of X,Y st card X = card Y holds
( F is onto iff F is one-to-one )

proof end;

Lm7: for n being Nat
for N being finite Subset of NAT
for F being Function of N, card N st n in N & F is bijective & ( for n, k being Nat st n in dom F & k in dom F & n < k holds
F . n < F . k ) holds
ex P being Permutation of N st
for k being Nat st k in N holds
( ( k < n implies P . k = (F " ) . ((F . k) + 1) ) & ( k = n implies P . k = (F " ) . 0 ) & ( k > n implies P . k = k ) )

proof end;

theorem Th71: :: STIRL2_1:71

for F, G being Function
for y being set st y in rng (G * F) & G is one-to-one holds
ex x being set st
( x in dom G & x in rng F & G " {y} = {x} & F " {x} = (G * F) " {y} )

proof end;

definition

let Ne, Ke be Subset of NAT ;
let f be Function of Ne,Ke;
attr f is "increasing means :Def5: :: STIRL2_1:def 5
for l, m being Nat st l in rng f & m in rng f & l < m holds
min* (f " {l}) < min* (f " {m});

end;

:: deftheorem Def5 defines "increasing STIRL2_1:def 5 :

theorem Th72: :: STIRL2_1:72

for Ne, Ke being Subset of NAT
for F being Function of Ne,Ke st F is "increasing holds
min* (rng F) = F . (min* (dom F))

proof end;

theorem :: STIRL2_1:73

for Ne, Ke being Subset of NAT
for F being Function of Ne,Ke st rng F is finite holds
ex I being Function of Ne,Ke ex P being Permutation of rng F st
( F = P * I & rng F = rng I & I is "increasing )

proof end;

theorem Th74: :: STIRL2_1:74

for Ne, Ke, Me being Subset of NAT
for F being Function of Ne,Ke st rng F is finite holds
for I1, I2 being Function of Ne,Me
for P1, P2 being Function st P1 is one-to-one & P2 is one-to-one & rng I1 = rng I2 & rng I1 = dom P1 & dom P1 = dom P2 & F = P1 * I1 & F = P2 * I2 & I1 is "increasing & I2 is "increasing holds
( P1 = P2 & I1 = I2 )

proof end;

theorem :: STIRL2_1:75

for Ne, Ke being Subset of NAT
for F being Function of Ne,Ke st rng F is finite holds
for I1, I2 being Function of Ne,Ke
for P1, P2 being Permutation of rng F st F = P1 * I1 & F = P2 * I2 & rng F = rng I1 & rng F = rng I2 & I1 is "increasing & I2 is "increasing holds
( P1 = P2 & I1 = I2 )

proof end;