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

registration
end;

registration

let X be non empty set ;

existence

ex b_{1} being Subset of X st

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

end;
existence

ex b

( b

proof end;

:: from AMI_1

:: from ALI2

theorem :: FINSET_1:11

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;

:: from FIN_TOPO

theorem :: FINSET_1:12

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;

:: 2006.08.25, A.T.

definition

let R be Relation;

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 ;

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

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

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

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;

:: restored, 2007.07.22, A.T.

registration
end;

registration
end;

:: from SCMFSA_4, 2007.07.22, A.T.

:: from SF_MASTR, 2007.07.25, A.T.

registration

let A be finite set ;

let B be set ;

coherence

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

end;
let B be set ;

coherence

for b

proof end;

:: from GLIB_000, 2007.10.24, A.T.

:: from FINSEQ_1, 2008.02.19, A.T.

registration
end;

:: from FINSEQ_1, 2008.05.06, A.T.

registration
end;

:: from COMPTS_1, 2008.07.16, A.T

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

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 f be Function;

( f is finite-yielding iff for i being object st i in dom f holds

f . i is finite )

end;
redefine attr f is finite-yielding means :Def4: :: FINSET_1:def 4

for i being object st i in dom f holds

f . i is finite ;

compatibility for i being object st i in dom f holds

f . i is finite ;

( f is finite-yielding iff for i being object st i in dom f holds

f . i is finite )

proof end;

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

for f being Function holds

( f is finite-yielding iff for i being object st i in dom f holds

f . i is finite );

for f being Function holds

( f is finite-yielding iff for i being object 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;

( IT is finite-yielding iff for i being object 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 5

for i being object st i in I holds

IT . i is finite ;

compatibility redefine attr IT is finite-yielding means :: FINSET_1:def 5

for i being object st i in I holds

IT . i is finite ;

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

IT . i is finite )

proof end;

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

for I being set

for IT being b_{1} -defined Function holds

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

IT . i is finite );

for I being set

for IT being b

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

IT . i is finite );

:: new, 2009.08.26, A.T

:: new, 2009.09.30, A.T.

registration

let I be set ;

let f be I -defined Function;

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;

existence

ex b

( b

proof end;

registration

let X, Y be set ;

existence

ex b_{1} being Function st

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

end;
existence

ex b

( b

proof end;

registration

let X, Y be non empty set ;

existence

ex b_{1} being Function st

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

end;
existence

ex b

( b

proof end;

registration
end;

registration
end;

registration

let X be non trivial set ;

existence

ex b_{1} being Subset of X st

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

end;
existence

ex b

( b

proof end;

:: 2011.04.07, A.T,

:: from MATROID0, 2011.07.25, A.T.

definition

let A be set ;

end;
attr A is finite-membered means :Def6: :: FINSET_1:def 6

for B being set st B in A holds

B is finite ;

for B being set st B in A holds

B is finite ;

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

for A being set holds

( A is finite-membered iff for B being set st B in A holds

B is finite );

registration

let A be finite-membered set ;

coherence

for b_{1} being Element of A holds b_{1} is finite

end;
coherence

for b

proof end;

registration

existence

ex b_{1} being set st

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

end;
ex b

( not b

proof end;

:: from SIMPLEX0, 2011.07.25, A.T.

registration

let X be finite set ;

coherence

{X} is finite-membered by TARSKI:def 1;

coherence

bool X is finite-membered ;

let Y be finite set ;

coherence

{X,Y} is finite-membered by TARSKI:def 2;

end;
coherence

{X} is finite-membered by TARSKI:def 1;

coherence

bool X is finite-membered ;

let Y be finite set ;

coherence

{X,Y} is finite-membered by TARSKI:def 2;

registration

let X be finite-membered set ;

coherence

for b_{1} being Subset of X holds b_{1} is finite-membered
;

let Y be finite-membered set ;

coherence

X \/ Y is finite-membered

end;
coherence

for b

let Y be finite-membered set ;

coherence

X \/ Y is finite-membered

proof end;

registration

existence

ex b_{1} being Function st

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

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

b_{1} is finite-yielding
;

end;
ex b

( not b

proof end;

coherence for b

b

registration
end;