:: Finite Sets
:: by Agata Darmochwa\l
::
:: Received April 6, 1989
:: Copyright (c) 1990-2018 Association of Mizar Users


definition
let IT be set ;
attr IT is finite means :Def1: :: FINSET_1:def 1
ex p being Function st
( rng p = IT & dom p in omega );
end;

:: deftheorem Def1 defines finite FINSET_1:def 1 :
for IT being set holds
( IT is finite iff ex p being Function st
( rng p = IT & dom p in omega ) );

notation
let IT be set ;
antonym infinite IT for finite ;
end;

Lm1: for x being object holds {x} is finite
proof end;

registration
cluster non empty finite for set ;
existence
ex b1 being set st
( not b1 is empty & b1 is finite )
proof end;
end;

registration
cluster empty -> finite for set ;
coherence
for b1 being set st b1 is empty holds
b1 is finite
proof end;
end;

scheme :: FINSET_1:sch 1
OLambdaC{ F1() -> set , P1[ object ], F2( object ) -> object , F3( object ) -> object } :
ex f being Function st
( dom f = F1() & ( for x being Ordinal st x in F1() holds
( ( P1[x] implies f . x = F2(x) ) & ( P1[x] implies f . x = F3(x) ) ) ) )
proof end;

Lm2: for A, B being set st A is finite & B is finite holds
A \/ B is finite

proof end;

registration
let x be object ;
cluster {x} -> finite ;
coherence
{x} is finite
by Lm1;
end;

registration
let x, y be object ;
cluster {x,y} -> finite ;
coherence
{x,y} is finite
proof end;
end;

registration
let x, y, z be object ;
cluster {x,y,z} -> finite ;
coherence
{x,y,z} is finite
proof end;
end;

registration
let x1, x2, x3, x4 be object ;
cluster {x1,x2,x3,x4} -> finite ;
coherence
{x1,x2,x3,x4} is finite
proof end;
end;

registration
let x1, x2, x3, x4, x5 be object ;
cluster {x1,x2,x3,x4,x5} -> finite ;
coherence
{x1,x2,x3,x4,x5} is finite
proof end;
end;

registration
let x1, x2, x3, x4, x5, x6 be object ;
cluster {x1,x2,x3,x4,x5,x6} -> finite ;
coherence
{x1,x2,x3,x4,x5,x6} is finite
proof end;
end;

registration
let x1, x2, x3, x4, x5, x6, x7 be object ;
cluster {x1,x2,x3,x4,x5,x6,x7} -> finite ;
coherence
{x1,x2,x3,x4,x5,x6,x7} is finite
proof end;
end;

registration
let x1, x2, x3, x4, x5, x6, x7, x8 be object ;
cluster {x1,x2,x3,x4,x5,x6,x7,x8} -> finite ;
coherence
{x1,x2,x3,x4,x5,x6,x7,x8} is finite
proof end;
end;

registration
let B be finite set ;
cluster -> finite for Subset of B;
coherence
for b1 being Subset of B holds b1 is finite
proof end;
end;

registration
let X, Y be finite set ;
cluster X \/ Y -> finite ;
coherence
X \/ Y is finite
by Lm2;
end;

theorem :: FINSET_1:1
for A, B being set st A c= B & B is finite holds
A is finite ;

theorem :: FINSET_1:2
for A, B being set st A is finite & B is finite holds
A \/ B is finite ;

registration
let A be set ;
let B be finite set ;
cluster A /\ B -> finite ;
coherence
A /\ B is finite
proof end;
end;

registration
let A be finite set ;
let B be set ;
cluster A /\ B -> finite ;
coherence
A /\ B is finite
;
cluster K30(A,B) -> finite ;
coherence
A \ B is finite
;
end;

theorem :: FINSET_1:3
for A, B being set st A is finite holds
A /\ B is finite ;

theorem :: FINSET_1:4
for A, B being set st A is finite holds
A \ B is finite ;

registration
let f be Function;
let A be finite set ;
cluster f .: A -> finite ;
coherence
f .: A is finite
proof end;
end;

theorem :: FINSET_1:5
for A being set
for f being Function st A is finite holds
f .: A is finite ;

theorem Th6: :: FINSET_1:6
for A being set st A is finite holds
for X being Subset-Family of A st X <> {} holds
ex x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) )
proof end;

scheme :: FINSET_1:sch 2
Finite{ F1() -> set , P1[ set ] } :
P1[F1()]
provided
A1: F1() is finite and
A2: P1[ {} ] and
A3: for x, B being set st x in F1() & B c= F1() & P1[B] holds
P1[B \/ {x}]
proof end;

Lm3: for A being set st A is finite & ( for X being set st X in A holds
X is finite ) holds
union A is finite

proof end;

registration
let A, B be finite set ;
cluster [:A,B:] -> finite ;
coherence
[:A,B:] is finite
proof end;
end;

registration
let A, B, C be finite set ;
cluster [:A,B,C:] -> finite ;
coherence
[:A,B,C:] is finite
proof end;
end;

registration
let A, B, C, D be finite set ;
cluster [:A,B,C,D:] -> finite ;
coherence
[:A,B,C,D:] is finite
proof end;
end;

registration
let A be finite set ;
cluster K32(A) -> finite ;
coherence
bool A is finite
proof end;
end;

theorem Th7: :: FINSET_1:7
for A being set holds
( ( A is finite & ( for X being set st X in A holds
X is finite ) ) iff union A is finite )
proof end;

theorem Th8: :: FINSET_1:8
for f being Function st dom f is finite holds
rng f is finite
proof end;

theorem