:: FINSET_1 semantic presentation

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 :

notation

let IT be set ;
antonym infinite IT for finite IT;

end;

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

proof end;

registration

cluster non empty finite set ;
existence

proof end;

end;

registration

cluster empty -> finite set ;
coherence

proof end;

end;

registration

let X be set ;
cluster empty finite Element of bool X;
existence

proof end;

end;

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

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 set ;
cluster {x} -> finite ;
coherence by Lm1;

end;

registration

let X be non empty set ;
cluster non empty finite Element of bool X;
existence

proof end;

end;

registration

let x, y be set ;
cluster {x,y} -> finite ;
coherence

proof end;

end;

registration

let x, y, z be set ;
cluster {x,y,z} -> finite ;
coherence

proof end;

end;

registration

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

proof end;

end;

registration

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

proof end;

end;

registration

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

proof end;

end;

registration

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

proof end;

end;

registration

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

proof end;

end;

registration

let B be finite set ;
cluster -> finite Element of bool B;
coherence

proof end;

end;

registration

let X, Y be finite set ;
cluster X \/ Y -> finite ;
coherence by Lm2;

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

for A, B being set st A c= B & B is finite holds
A is finite

proof end;

theorem :: FINSET_1:14

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

registration

let A be set ;
let B be finite set ;
cluster A /\ B -> finite ;
coherence

proof end;

end;

registration

let A be finite set ;
let B be set ;
cluster A /\ B -> finite ;
coherence ;
cluster A \ B -> finite ;
coherence

proof end;

end;

theorem Th15: :: FINSET_1:15

for A, B being set st A is finite holds
A /\ B is finite

proof end;

theorem Th16: :: FINSET_1:16

for A, B being set st A is finite holds
A \ B is finite

proof end;

theorem Th17: :: FINSET_1:17

for A being set
for f being Function st A is finite holds
f .: A is finite

proof end;

registration

let f be Function;
let A be finite set ;
cluster f .: A -> finite ;
coherence by Th17;

end;

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

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;

theorem Th19: :: FINSET_1:19

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

proof end;

registration

let A, B be finite set ;
cluster [:A,B:] -> finite ;
coherence by Th19;

end;

theorem Th20: :: FINSET_1:20

for A, B, C being set st A is finite & B is finite & C is finite holds
[:A,B,C:] is finite

proof end;

registration

let A, B, C be finite set ;
cluster [:A,B,C:] -> finite ;
coherence by Th20;

end;

theorem Th21: :: FINSET_1:21

for A, B, C, D being set st A is finite & B is finite & C is finite & D is finite holds
[:A,B,C,D:] is finite

proof end;

registration

let A, B, C, D be finite set ;
cluster [:A,B,C,D:] -> finite ;
coherence by Th21;

end;

theorem :: FINSET_1:22

for B, A being set st B <> {} & [:A,B:] is finite holds
A is finite

proof end;

theorem :: FINSET_1:23

for A, B being set st A <> {} & [:A,B:] is finite holds
B is finite

proof end;

theorem Th24: :: FINSET_1:24

for A being set holds
( A is finite iff bool A is finite )

proof end;

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 )

proof end;

theorem Th26: :: FINSET_1:26

for f being Function st dom f is finite holds
rng f is finite

proof end;

theorem :: FINSET_1:27

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

proof end;

theorem :: FINSET_1:28

for X, Y being set st X is finite & Y is finite holds
X \+\ Y is finite

proof end;

registration

let X, Y be finite set ;
cluster X \+\ Y -> finite ;
coherence ;

end;

registration

let X be non empty set ;
cluster non empty finite Element of bool X;
existence

proof end;

end;

theorem :: FINSET_1:29

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

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

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

proof end;