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


begin

definition
let IT be set ;
attrIT 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 set holds {x} is finite
proofend;

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

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

scheme :: FINSET_1:sch 1
OLambdaC{ F1() ->  set , P1[ set ], F2( set ) ->  set , F3( set ) ->  set } :
 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) ) ) ) )
proofend;

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

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

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

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

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

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

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

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

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

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

registration
let X, Y be finite set ;
clusterX \/ 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 ;
clusterA /\ B ->  finite ;
coherence
 A /\ B is finite
proofend;
end;

registration
let A be finite set ;
let B be set ;
clusterA /\ B ->  finite ;
coherence
 A /\ B is finite ;
clusterA \ 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 ;
clusterf .: A ->  finite ;
coherence
 f .: A is finite
proofend;
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 &amp; ( for B being set st B in X &amp; x c= B holds
B = x ) )
proofend;

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() &amp; B c= F1() &amp; P1[B] holds
P1[B \/ {x}]
proofend;

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

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

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

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

registration
let A be finite set ;
cluster bool A ->  finite ;
coherence
 bool A is finite
proofend;
end;

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

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

theorem :: FINSET_1:9
for Y being set
for f being Function st Y c= rng f &amp; f " Y is finite holds
Y is finite
proofend;

registration
let X, Y be finite set ;
clusterX \+\ Y ->  finite ;
coherence
 X \+\ Y is finite ;
end;

registration
let X be non empty set ;
cluster non empty finite for Element of bool X;
existence
 ex b1 being Subset of X st
( b1 is finite &amp; not b1 is empty )
proofend;
end;

begin

:: from AMI_1
theorem Th10: :: FINSET_1:10
for f being Function holds
( dom f is finite iff f is finite )
proofend;

:: from ALI2
theorem :: FINSET_1:11
for F being set st F is finite &amp; F <> {} &amp; F is c=-linear holds
ex m being set st
( m in F &amp; ( for C being set st C in F holds
m c= C ) )
proofend;

:: from FIN_TOPO
theorem :: FINSET_1:12
for F being set st F is finite &amp; F <> {} &amp; F is c=-linear holds
ex m being set st
( m in F &amp; ( for C being set st C in F holds
C c= m ) )
proofend;

:: 2006.08.25, A.T.
definition
let R be Relation;
attrR is finite-yielding  means :Def2: :: FINSET_1:def 2
 for x being set st x in rng R holds
x is finite ;
end;

:: deftheorem Def2 defines finite-yielding FINSET_1:def_2_:_
 for R being Relation holds
( R is finite-yielding iff for x being set st x in rng R holds
x is finite );

deffunc H1( set ) ->  set = $1 `1 ;

theorem :: FINSET_1:13
for X, Y, Z being set st X is finite &amp; X c= [:Y,Z:] holds
ex A, B being set st
( A is finite &amp; A c= Y &amp; B is finite &amp; B c= Z &amp; X c= [:A,B:] )
proofend;

theorem :: FINSET_1:14
for X, Y, Z being set st X is finite &amp; X c= [:Y,Z:] holds
ex A being set st
( A is finite &amp; A c= Y &amp; X c= [:A,Z:] )
proofend;

:: restored, 2007.07.22, A.T.
registration
cluster non empty Relation-like Function-like finite for set ;
existence
 ex b1 being Function st
( b1 is finite &amp; not b1 is empty )
proofend;
end;

registration
let R be finite Relation;
cluster proj1 R ->  finite ;
coherence
 dom R is finite
proofend;
end;

:: from SCMFSA_4, 2007.07.22, A.T.
registration
let f be Function;
let g be finite Function;
clusterg * f ->  finite ;
coherence
 f * g is finite
proofend;
end;

:: from SF_MASTR, 2007.07.25, A.T.
registration
let A be finite set ;
let B be set ;
cluster Function-like V18(A,B)  ->  finite for Element of bool [:A,B:];
coherence
 for b1 being Function of A,B holds b1 is finite
proofend;
end;

:: from GLIB_000, 2007.10.24, A.T.
registration
let x, y be set ;
clusterx .--> y ->  finite ;
coherence
 x .--> y is finite ;
end;

:: from FINSEQ_1, 2008.02.19, A.T.
registration
let R be finite Relation;
cluster proj2 R ->  finite ;
coherence
 rng R is finite
proofend;
end;

:: from FINSEQ_1, 2008.05.06, A.T.
registration
let f be finite Function;
let x be set ;
clusterf " x ->  finite ;
coherence
 f " x is finite
proofend;
end;

registration
let f, g be finite Function;
clusterf +* g ->  finite ;
coherence
 f +* g is finite
proofend;
end;

:: from COMPTS_1, 2008.07.16, A.T
definition
let F be set ;
attrF is centered  means :: FINSET_1:def 3
( F <> {} &amp; ( for G being set st G <> {} &amp; G c= F &amp; G is finite holds
meet G <> {} ) );
end;

:: deftheorem  defines centered FINSET_1:def_3_:_
 for F being set holds
( F is centered iff ( F <> {} &amp; ( for G being set st G <> {} &amp; G c= F &amp; G is finite holds
meet G <> {} ) ) );

definition
let f be Function;
redefine attr f is finite-yielding  means :Def4: :: FINSET_1:def 4
 for i being set st i in dom f holds
f . i is finite ;
compatibility
 ( f is finite-yielding iff for i being set st i in dom f holds
f . i is finite )
proofend;
end;

:: deftheorem Def4 defines finite-yielding FINSET_1:def_4_:_
 for f being Function holds
( f is finite-yielding iff for i being set st i in dom f holds
f . i is finite );

:: from PRE_CIRC, 2009.03.04, A.T.
definition
let I be set ;
let IT be I -defined Function;
:: original:finite-yielding
redefine attrIT is finite-yielding  means :: FINSET_1:def 5
 for i being set st i in I holds
IT . i is finite ;
compatibility
 ( IT is finite-yielding iff for i being set st i in I holds
IT . i is finite )
proofend;
end;

:: deftheorem  defines finite-yielding FINSET_1:def_5_:_
 for I being set
for IT being b1 -defined Function holds
( IT is finite-yielding iff for i being set st i in I holds
IT . i is finite );

:: new, 2009.08.26, A.T
theorem :: FINSET_1:15
for B, A being set st B is infinite holds
not B in [:A,B:]
proofend;

:: new, 2009.09.30, A.T.
registration
let I be set ;
let f be I -defined Function;
cluster Relation-like I -defined Function-like f -compatible finite for set ;
existence
 ex b1 being Function st
( b1 is finite &amp; b1 is I -defined &amp; b1 is f -compatible )
proofend;
end;

registration
let X, Y be set ;
cluster Relation-like X -defined Y -valued Function-like finite for set ;
existence
 ex b1 being Function st
( b1 is finite &amp; b1 is X -defined &amp; b1 is Y -valued )
proofend;
end;

registration
let X, Y be non empty set ;
cluster non empty Relation-like X -defined Y -valued Function-like finite for set ;
existence
 ex b1 being Function st
( b1 is X -defined &amp; b1 is Y -valued &amp; not b1 is empty &amp; b1 is finite )
proofend;
end;

registration
let A be set ;
let F be finite Relation;
clusterA |` F ->  finite ;
coherence
 A |` F is finite
proofend;
end;

registration
let A be set ;
let F be finite Relation;
clusterF | A ->  finite ;
coherence
 F | A is finite
proofend;
end;

registration
let A be finite set ;
let F be Function;
clusterF | A ->  finite ;
coherence
 F | A is finite
proofend;
end;

registration
let R be finite Relation;
cluster field R ->  finite ;
coherence
 field R is finite ;
end;

registration
cluster trivial  ->  finite for set ;
coherence
 for b1 being set st b1 is trivial holds
b1 is finite
proofend;
end;

registration
cluster infinite  ->  non trivial for set ;
coherence
 for b1 being set st b1 is infinite holds
not b1 is trivial ;
end;

registration
let X be non trivial set ;
cluster non trivial finite for Element of bool X;
existence
 ex b1 being Subset of X st
( b1 is finite &amp; not b1 is trivial )
proofend;
end;

:: 2011.04.07, A.T,
registration
let x, y, a, b be set ;
cluster(x,y) --> (a,b) ->  finite ;
coherence
 (x,y) --> (a,b) is finite ;
end;

:: from MATROID0, 2011.07.25, A.T.
definition
let A be set ;
attrA is finite-membered  means :Def6: :: FINSET_1:def 6
 for B being set st B in A holds
B is finite ;
end;

:: deftheorem Def6 defines finite-membered FINSET_1:def_6_:_
 for A being set holds
( A is finite-membered iff for B being set st B in A holds
B is finite );

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

registration
let A be finite-membered set ;
cluster  ->  finite for Element of A;
coherence
 for b1 being Element of A holds b1 is finite
proofend;
end;

registration
cluster non empty finite finite-membered for set ;
existence
 ex b1 being set st
( not b1 is empty &amp; b1 is finite &amp; b1 is finite-membered )
proofend;
end;

:: from SIMPLEX0, 2011.07.25, A.T.
registration
let X be finite set ;
cluster{X} ->  finite-membered ;
coherence
 {X} is finite-membered
proofend;
cluster bool X ->  finite-membered ;
coherence
 bool X is finite-membered
proofend;
let Y be finite set ;
cluster{X,Y} ->  finite-membered ;
coherence
 {X,Y} is finite-membered
proofend;
end;

registration
let X be finite-membered set ;
cluster  ->  finite-membered for Element of bool X;
coherence
 for b1 being Subset of X holds b1 is finite-membered
proofend;
let Y be finite-membered set ;
clusterX \/ Y ->  finite-membered ;
coherence
 X \/ Y is finite-membered
proofend;
end;

registration
let X be finite finite-membered set ;
cluster union X ->  finite ;
coherence
 union X is finite
proofend;
end;

registration
cluster non empty Relation-like Function-like finite-yielding for set ;
existence
 ex b1 being Function st
( not b1 is empty &amp; b1 is finite-yielding )
proofend;
cluster empty Relation-like  ->  finite-yielding for set ;
coherence
 for b1 being Relation st b1 is empty holds
b1 is finite-yielding
proofend;
end;

registration
let F be finite-yielding Function;
let x be set ;
clusterF . x ->  finite ;
coherence
 F . x is finite
proofend;
end;

registration
let F be finite-yielding Relation;
cluster proj2 F ->  finite-membered ;
coherence
 rng F is finite-membered
proofend;
end;