:: by Agata Darmochwa\l

::

:: Received April 6, 1989

:: Copyright (c) 1990-2018 Association of Mizar Users

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

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 object holds {x} is finite

proof end;

registration
end;

scheme :: FINSET_1:sch 1

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

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

registration
end;

registration
end;

registration
end;

registration

let x1, x2, x3, x4, x5, x6, x7, x8 be object ;

coherence

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

end;
coherence

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

proof end;

registration
end;

registration
end;

registration
end;

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

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;

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

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

X is finite ) ) iff union A is finite )

proof end;