Volume 1, 1989

University of Bialystok

Copyright (c) 1989 Association of Mizar Users

### The abstract of the Mizar article:

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