Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989 Association of Mizar Users

### Finite Sets

by
Agata Darmochwal

Received April 6, 1989

MML identifier: FINSET_1
[ Mizar article, MML identifier index ]

```environ

vocabulary FUNCT_1, RELAT_1, ORDINAL2, BOOLE, ORDINAL1, ORDINAL3, SETFAM_1,
TARSKI, MCART_1, FINSET_1;
notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1,
MCART_1, SETFAM_1, ORDINAL1, ORDINAL2, ORDINAL3;
constructors ENUMSET1, MCART_1, ORDINAL3, SETFAM_1, XBOOLE_0;
clusters FUNCT_1, ORDINAL2, RELAT_1, ARYTM_3, ORDINAL1, SUBSET_1, ZFMISC_1,
XBOOLE_0;
requirements SUBSET, BOOLE;

begin

definition let IT be set;
attr IT is finite means
:: FINSET_1:def 1
ex p being Function st rng p = IT & dom p in omega;
antonym IT is infinite;
end;

reserve A, B, C, D, X, Y, Z, x, y for set;
reserve f for Function;

definition
cluster non empty finite set;
end;

definition
cluster empty -> finite set;
end;

definition let X be set;
cluster empty finite Subset of X;
end;

scheme OLambdaC{A()->set,C[set],F(set)->set,G(set)->set}:
ex f being Function st dom f = A() &
for x being Ordinal st x in A() holds
(C[x] implies f.x = F(x)) & (not C[x] implies f.x = G(x));

definition let x be set;
cluster {x} -> finite;
end;

definition let X be non empty set;
cluster non empty finite Subset of X;
end;

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

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

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

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

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

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

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

definition let B be finite set;
cluster -> finite Subset of B;
end;

definition let X,Y be finite set;
cluster X \/ Y -> finite;
end;

canceled 12;

theorem :: FINSET_1:13
A c= B & B is finite implies A is finite;

theorem :: FINSET_1:14
A is finite & B is finite implies A \/ B is finite;

definition let A be set, B be finite set;
cluster A /\ B -> finite;
end;

definition let A be finite set, B be set;
cluster A /\ B -> finite;
cluster A \ B -> finite;
end;

theorem :: FINSET_1:15
A is finite implies A /\ B is finite;

theorem :: FINSET_1:16
A is finite implies A \ B is finite;

theorem :: FINSET_1:17
A is finite implies f.:A is finite;

definition let f be Function, A be finite set;
cluster f.:A -> finite;
end;

reserve O for Ordinal;

theorem :: FINSET_1:18
A is finite implies for X being Subset-Family of A st X <> {}
ex x being set st
x in X & for B being set st B in X holds x c= B implies B = x;

scheme Finite{A()->set,P[set]} : P[A()]
provided
A() is finite and
P[{}] and
for x,B being set st x in A() & B c= A() & P[B] holds P[B \/ {x}];

theorem :: FINSET_1:19
A is finite & B is finite implies [:A,B:] is finite;

definition let A,B be finite set;
cluster [:A,B:] -> finite;
end;

theorem :: FINSET_1:20
A is finite & B is finite & C is finite
implies [:A,B,C:] is finite;

definition let A,B,C be finite set;
cluster [:A,B,C:] -> finite;
end;

theorem :: FINSET_1:21
A is finite & B is finite & C is finite & D is finite
implies [:A,B,C,D:] is finite;

definition let A,B,C,D be finite set;
cluster [:A,B,C,D:] -> finite;
end;

theorem :: FINSET_1:22
B <> {} & [:A,B:] is finite implies A is finite;

theorem :: FINSET_1:23
A <> {} & [:A,B:] is finite implies B is finite;

theorem :: FINSET_1:24
A is finite iff bool A is finite;

theorem :: FINSET_1:25
A is finite & (for X st X in A holds X is finite) iff union A is finite;

theorem :: FINSET_1:26
dom f is finite implies rng f is finite;

theorem :: FINSET_1:27
Y c= rng f & f"Y is finite implies Y is finite;
```

Back to top