:: by Agata Darmochwa\l

::

:: Received April 6, 1989

:: Copyright (c) 1990 Association of Mizar Users

begin

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;
attr IT is finite means :Def1: :: FINSET_1:def 1

ex p being Function st

( rng p = IT & dom p in omega );

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

Lm1: for x being set holds {x} is finite

proof end;

registration

cluster non empty finite set ;

existence

ex b_{1} being set st

( not b_{1} is empty & b_{1} is finite )

end;
existence

ex b

( not b

proof end;

registration

cluster empty -> finite set ;

coherence

for b_{1} being set st b_{1} is empty holds

b_{1} is finite

end;
coherence

for b

b

proof end;

scheme :: FINSET_1:sch 1

OLambdaC{ F_{1}() -> set , P_{1}[ set ], F_{2}( set ) -> set , F_{3}( set ) -> set } :

OLambdaC{ F

ex f being Function st

( dom f = F_{1}() & ( for x being Ordinal st x in F_{1}() holds

( ( P_{1}[x] implies f . x = F_{2}(x) ) & ( P_{1}[x] implies f . x = F_{3}(x) ) ) ) )

( dom f = F

( ( P

proof end;

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

A \/ B is finite

proof end;

registration
end;

registration

let x1, x2, x3, x4 be set ;

cluster {x1,x2,x3,x4} -> finite ;

coherence

{x1,x2,x3,x4} is finite

end;
cluster {x1,x2,x3,x4} -> finite ;

coherence

{x1,x2,x3,x4} is finite

proof 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

end;
cluster {x1,x2,x3,x4,x5} -> finite ;

coherence

{x1,x2,x3,x4,x5} is finite

proof 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

end;
cluster {x1,x2,x3,x4,x5,x6} -> finite ;

coherence

{x1,x2,x3,x4,x5,x6} is finite

proof 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

end;
cluster {x1,x2,x3,x4,x5,x6,x7} -> finite ;

coherence

{x1,x2,x3,x4,x5,x6,x7} is finite

proof 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

end;
cluster {x1,x2,x3,x4,x5,x6,x7,x8} -> finite ;

coherence

{x1,x2,x3,x4,x5,x6,x7,x8} is finite

proof end;

registration

let B be finite set ;

cluster -> finite Element of bool B;

coherence

for b_{1} being Subset of B holds b_{1} is finite

end;
cluster -> finite Element of bool B;

coherence

for b

proof end;

registration
end;

theorem :: FINSET_1:1

canceled;

theorem :: FINSET_1:2

canceled;

theorem :: FINSET_1:3

canceled;

theorem :: FINSET_1:4

canceled;

theorem :: FINSET_1:5

canceled;

theorem :: FINSET_1:6

canceled;

theorem :: FINSET_1:7

canceled;

theorem :: FINSET_1:8

canceled;

theorem :: FINSET_1:9

canceled;

theorem :: FINSET_1:10

canceled;

theorem :: FINSET_1:11

canceled;

theorem :: FINSET_1:12

canceled;

theorem :: FINSET_1:13

theorem :: FINSET_1:14

registration

let A be set ;

let B be finite set ;

cluster A /\ B -> finite ;

coherence

A /\ B is finite

end;
let B be finite set ;

cluster A /\ B -> finite ;

coherence

A /\ B is finite

proof end;

registration

let A be finite set ;

let B be set ;

cluster A /\ B -> finite ;

coherence

A /\ B is finite ;

cluster A \ B -> finite ;

coherence

A \ B is finite ;

end;
let B be set ;

cluster A /\ B -> finite ;

coherence

A /\ B is finite ;

cluster A \ B -> finite ;

coherence

A \ B is finite ;

theorem :: FINSET_1:15

theorem :: FINSET_1:16

registration

let f be Function;

let A be finite set ;

cluster f .: A -> finite ;

coherence

f .: A is finite

end;
let A be finite set ;

cluster f .: A -> finite ;

coherence

f .: A is finite

proof end;

theorem :: FINSET_1:17

theorem Th18: :: FINSET_1:18

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

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{ F_{1}() -> set , P_{1}[ set ] } :

provided

Finite{ F

provided

A1:
F_{1}() is finite
and

A2: P_{1}[ {} ]
and

A3: for x, B being set st x in F_{1}() & B c= F_{1}() & P_{1}[B] holds

P_{1}[B \/ {x}]

A2: P

A3: for x, B being set st x in F

P

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
end;

registration
end;

registration

let A, B, C, D be finite set ;

cluster [:A,B,C,D:] -> finite ;

coherence

[:A,B,C,D:] is finite

end;
cluster [:A,B,C,D:] -> finite ;

coherence

[:A,B,C,D:] is finite

proof end;

registration
end;

theorem :: FINSET_1:19

canceled;

theorem :: FINSET_1:20

canceled;

theorem :: FINSET_1:21

canceled;

theorem :: FINSET_1:22

canceled;

theorem :: FINSET_1:23

canceled;

theorem :: FINSET_1:24

canceled;

theorem :: FINSET_1:25

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 )

( ( A is finite & ( for X being set st X in A holds

X is finite ) ) iff union A is finite )

proof end;

theorem Th26: :: FINSET_1:26

proof end;

theorem :: FINSET_1:27

proof end;

registration
end;

registration

let X be non empty set ;

cluster non empty finite Element of bool X;

existence

ex b_{1} being Subset of X st

( b_{1} is finite & not b_{1} is empty )

end;
cluster non empty finite Element of bool X;

existence

ex b

( b

proof end;

begin

theorem :: FINSET_1:28

canceled;

theorem Th29: :: FINSET_1:29

proof end;

theorem :: FINSET_1:30

for F being set st F is finite & F <> {} & F is c=-linear holds

ex m being set st

( m in F & ( for C being set st C in F holds

m c= C ) )

ex m being set st

( m in F & ( for C being set st C in F holds

m c= C ) )

proof end;

theorem :: FINSET_1:31

for F being set st F is finite & F <> {} & F is c=-linear holds

ex m being set st

( m in F & ( for C being set st C in F holds

C c= m ) )

ex m being set st

( m in F & ( for C being set st C in F holds

C c= m ) )

proof end;

definition

let R be Relation;

attr R is finite-yielding means :Def2: :: FINSET_1:def 2

for x being set st x in rng R holds

x is finite ;

end;
attr R is finite-yielding means :Def2: :: FINSET_1:def 2

for x being set st x in rng R holds

x is finite ;

:: 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 H

theorem :: FINSET_1:32

for X, Y, Z being set st X is finite & X c= [:Y,Z:] holds

ex A, B being set st

( A is finite & A c= Y & B is finite & B c= Z & X c= [:A,B:] )

ex A, B being set st

( A is finite & A c= Y & B is finite & B c= Z & X c= [:A,B:] )

proof end;

theorem :: FINSET_1:33

for X, Y, Z being set st X is finite & X c= [:Y,Z:] holds

ex A being set st

( A is finite & A c= Y & X c= [:A,Z:] )

ex A being set st

( A is finite & A c= Y & X c= [:A,Z:] )

proof end;

registration

cluster non empty Relation-like Function-like finite set ;

existence

ex b_{1} being Function st

( b_{1} is finite & not b_{1} is empty )

end;
existence

ex b

( b

proof end;

registration
end;

registration

let f be Function;

let g be finite Function;

cluster g * f -> finite ;

coherence

f * g is finite

end;
let g be finite Function;

cluster g * f -> finite ;

coherence

f * g is finite

proof end;

registration

let A be finite set ;

let B be set ;

cluster Function-like V15(A,B) -> finite Element of bool [:A,B:];

coherence

for b_{1} being Function of A,B holds b_{1} is finite

end;
let B be set ;

cluster Function-like V15(A,B) -> finite Element of bool [:A,B:];

coherence

for b

proof end;

registration
end;

registration

let f be finite Function;

let x be set ;

cluster f " x -> finite ;

coherence

f " x is finite

end;
let x be set ;

cluster f " x -> finite ;

coherence

f " x is finite

proof end;

registration
end;

definition

let F be set ;

attr F is centered means :: FINSET_1:def 3

( F <> {} & ( for G being set st G <> {} & G c= F & G is finite holds

meet G <> {} ) );

end;
attr F is centered means :: FINSET_1:def 3

( F <> {} & ( for G being set st G <> {} & G c= F & G is finite holds

meet G <> {} ) );

:: deftheorem defines centered FINSET_1:def 3 :

for F being set holds

( F is centered iff ( F <> {} & ( for G being set st G <> {} & G c= F & G is finite holds

meet G <> {} ) ) );

definition

let I be set ;

let IT be I -defined Function;

:: original: finite-yielding

redefine attr IT is finite-yielding means :: FINSET_1:def 4

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 )

end;
let IT be I -defined Function;

:: original: finite-yielding

redefine attr IT is finite-yielding means :: FINSET_1:def 4

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 )

proof end;

:: deftheorem defines finite-yielding FINSET_1:def 4 :

for I being set

for IT being b

( IT is finite-yielding iff for i being set st i in I holds

IT . i is finite );

theorem :: FINSET_1:34

proof end;

registration

let I be set ;

let f be I -defined Function;

cluster Relation-like I -defined Function-like f -compatible finite set ;

existence

ex b_{1} being Function st

( b_{1} is finite & b_{1} is I -defined & b_{1} is f -compatible )

end;
let f be I -defined Function;

cluster Relation-like I -defined Function-like f -compatible finite set ;

existence

ex b

( b

proof end;

registration

let X, Y be set ;

cluster Relation-like X -defined Y -valued Function-like finite set ;

existence

ex b_{1} being Function st

( b_{1} is finite & b_{1} is X -defined & b_{1} is Y -valued )

end;
cluster Relation-like X -defined Y -valued Function-like finite set ;

existence

ex b

( b

proof end;

registration

let A be set ;

let F be finite Relation;

cluster A | F -> finite ;

coherence

A | F is finite

end;
let F be finite Relation;

cluster A | F -> finite ;

coherence

A | F is finite

proof end;

registration

let A be set ;

let F be finite Relation;

cluster F | A -> finite ;

coherence

F | A is finite

end;
let F be finite Relation;

cluster F | A -> finite ;

coherence

F | A is finite

proof end;

registration

let A be finite set ;

let F be Function;

cluster F | A -> finite ;

coherence

F | A is finite

end;
let F be Function;

cluster F | A -> finite ;

coherence

F | A is finite

proof end;

registration
end;