:: Finite Sets
:: by Agata Darmochwa\l
::
:: Received April 6, 1989
:: Copyright (c) 1990-2021 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 b₁ being set st
( not b₁ is empty & b₁ is finite )

proof end;

end;

registration

cluster empty -> finite for set ;

coherence
for b₁ being set st b₁ is empty holds
b₁ is finite

proof end;

end;

scheme :: FINSET_1:sch 1
OLambdaC{ F₁() -> set , P₁[ object ], F₂( object ) -> object , F₃( object ) -> object } :

ex f being Function st
( dom f = F₁() & ( for x being Ordinal st x in F₁() holds
( ( P₁[x] implies f . x = F₂(x) ) & ( P₁[x] implies f . x = F₃(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 Element of bool B;

coherence
for b₁ being Subset of B holds b₁ 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 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{ F₁() -> set , P₁[ set ] } :

P₁[F₁()]

provided

A1: F₁() is finite and
A2: P₁[ {} ] and
A3: for x, B being set st x in F₁() & B c= F₁() & P₁[B] holds
P₁[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 bool 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 :: FINSET_1:9

for Y being set
for f being Function st Y c= rng f & f " Y is finite holds
Y is finite

proof end;

registration

let X, Y be finite set ;

cluster X \+\ Y -> finite ;

coherence
X \+\ Y is finite ;

end;

registration

let X be set ;

cluster finite for Element of bool X;

existence
ex b₁ being Subset of X st b₁ is finite

proof end;

end;

registration

let X be non empty set ;

cluster non empty finite for Element of bool X;

existence
ex b₁ being Subset of X st
( b₁ is finite & not b₁ is empty )

proof end;

end;

:: from AMI_1

theorem Th10: :: FINSET_1:10

for f being Function holds
( dom f is finite iff f is finite )

proof end;

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

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

proof end;

:: 2006.08.25, A.T.

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;

:: 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₁( object ) -> object = $1 `1 ;

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

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

proof end;

:: restored, 2007.07.22, A.T.

registration

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

existence
ex b₁ being Function st
( b₁ is finite & not b₁ is empty )

proof end;

end;

registration

let R be finite Relation;

cluster proj1 R -> finite ;

coherence
dom R is finite

proof end;

end;

:: from SCMFSA_4, 2007.07.22, A.T.

registration

let f be Function;
let g be finite Function;

cluster g * f -> finite ;

coherence
f * g is finite

proof end;

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 b₁ being Function of A,B holds b₁ is finite

proof end;

end;

:: from GLIB_000, 2007.10.24, A.T.

registration

let x, y be object ;

cluster x .--> 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

proof end;

end;

:: from FINSEQ_1, 2008.05.06, A.T.

registration

let f be finite Function;
let x be set ;

cluster f " x -> finite ;

coherence
f " x is finite

proof end;

end;

registration

let f, g be finite Function;

cluster f +* g -> finite ;

coherence
f +* g is finite

proof end;

end;

:: from COMPTS_1, 2008.07.16, A.T

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;

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

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
( f is finite-yielding iff for i being object st i in dom f holds
f . i is finite )

proof end;

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

:: from PRE_CIRC, 2009.03.04, A.T.

definition

let I be set ;
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
( IT is finite-yielding iff for i being object st i in I holds
IT . i is finite )

proof end;

end;

:: deftheorem defines finite-yielding FINSET_1:def 5 :
for I being set
for IT being b₁ -defined Function holds
( IT is finite-yielding iff for i being object st i in I holds
IT . i is finite );

:: new, 2009.08.26, A.T

theorem :: FINSET_1:15

for A, B being set st B is infinite holds
not B in [:A,B:]

proof end;

:: 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 b₁ being Function st
( b₁ is finite & b₁ is I -defined & b₁ is f -compatible )

proof end;

end;

registration

let X, Y be set ;

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

existence
ex b₁ being Function st
( b₁ is finite & b₁ is X -defined & b₁ is Y -valued )

proof end;

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 b₁ being Function st
( b₁ is X -defined & b₁ is Y -valued & not b₁ is empty & b₁ is finite )

proof end;

end;

registration

let A be set ;
let F be finite Relation;

cluster A |` F -> finite ;

coherence
A |` F is finite

proof end;

end;

registration

let A be set ;
let F be finite Relation;

cluster F | A -> finite ;

coherence
F | A is finite

proof end;

end;

registration

let A be finite set ;
let F be Function;

cluster F | A -> finite ;

coherence
F | A is finite

proof end;

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 b₁ being set st b₁ is trivial holds
b₁ is finite

proof end;

end;

registration

cluster infinite -> non trivial for set ;

coherence
for b₁ being set st b₁ is infinite holds
not b₁ is trivial ;

end;

registration

let X be non trivial set ;

cluster non trivial finite for Element of bool X;

existence
ex b₁ being Subset of X st
( b₁ is finite & not b₁ is trivial )

proof end;

end;

:: 2011.04.07, A.T,

registration

let x, y, a, b be object ;

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 ;

attr A 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 b₁ being set st b₁ is empty holds
b₁ is finite-membered ;

end;

registration

let A be finite-membered set ;

cluster -> finite for Element of A;

coherence
for b₁ being Element of A holds b₁ is finite

proof end;

end;

registration

cluster non empty finite finite-membered for set ;

existence
ex b₁ being set st
( not b₁ is empty & b₁ is finite & b₁ is finite-membered )

proof end;

end;

:: from SIMPLEX0, 2011.07.25, A.T.

registration

let X be finite set ;

cluster {X} -> finite-membered ;

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

cluster bool X -> finite-membered ;

coherence
bool X is finite-membered ;
let Y be finite set ;

cluster {X,Y} -> finite-membered ;

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

end;

registration

let X be finite-membered set ;

cluster -> finite-membered for Element of bool X;

coherence
for b₁ being Subset of X holds b₁ is finite-membered ;
let Y be finite-membered set ;

cluster X \/ Y -> finite-membered ;

coherence
X \/ Y is finite-membered

proof end;

end;

registration

let X be finite finite-membered set ;

cluster union X -> finite ;

coherence
union X is finite

proof end;

end;

registration

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

existence
ex b₁ being Function st
( not b₁ is empty & b₁ is finite-yielding )

proof end;

cluster empty Relation-like -> finite-yielding for set ;

coherence
for b₁ being Relation st b₁ is empty holds
b₁ is finite-yielding ;

end;

registration

let F be finite-yielding Function;
let x be object ;

cluster F . x -> finite ;

coherence
F . x is finite

proof end;

end;

registration

let F be finite-yielding Relation;

cluster proj2 F -> finite-membered ;

coherence
rng F is finite-membered by Def2;

end;