:: Finite Sets
:: by Agata Darmochwa\l
::
:: Received April 6, 1989
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies FUNCT_1, RELAT_1, ORDINAL1, XBOOLE_0, FUNCOP_1, ORDINAL3,
ORDINAL2, TARSKI, SUBSET_1, SETFAM_1, ZFMISC_1, MCART_1, FUNCT_4,
FINSET_1, MATROID0, CARD_1;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, XTUPLE_0, RELAT_1, FUNCT_1,
FUNCOP_1, MCART_1, SETFAM_1, ORDINAL1, ORDINAL2, ORDINAL3, SUBSET_1,
DOMAIN_1, RELSET_1, FUNCT_2, FUNCT_3, FUNCT_4;
constructors DOMAIN_1, FUNCT_3, FUNCOP_1, ORDINAL3, FUNCT_4, SETFAM_1,
RELSET_1, XTUPLE_0;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, ORDINAL2,
RELSET_1, FUNCOP_1, XTUPLE_0;
requirements SUBSET, BOOLE, NUMERALS;
definitions TARSKI, XBOOLE_0;
equalities TARSKI, XBOOLE_0, FUNCOP_1, RELAT_1, FUNCT_4, ORDINAL1;
expansions TARSKI, XBOOLE_0, ORDINAL1;
theorems FUNCT_1, ENUMSET1, ZFMISC_1, TARSKI, RELAT_1, ORDINAL3, ORDINAL1,
XBOOLE_0, XBOOLE_1, FUNCT_3, FUNCOP_1, FUNCT_4, SUBSET_1, XTUPLE_0;
schemes FUNCT_1, PARTFUN1, ORDINAL2, XFAMILY;
begin
definition
let IT be set;
attr IT is finite means
:Def1:
ex p being Function st rng p = IT & dom p in omega;
end;
notation
let IT be set;
antonym IT is infinite for IT is finite;
end;
reserve A, B, X, Y, Z, x, y for set;
reserve f for Function;
Lm1:
for x being object holds {x} is finite
proof let x be object;
set p = {{}} --> x;
take p;
for y being object holds y in {x}
iff ex x being object st x in dom p & y = p.x
proof
let y be object;
thus y in {x} implies ex x being object st x in dom p & y = p.x
proof
assume y in {x};
then
A2: y = x by TARSKI:def 1;
take {};
thus {} in dom p by TARSKI:def 1;
{} in {{}} by TARSKI:def 1;
hence thesis by A2,FUNCOP_1:7;
end;
assume ex z be object st z in dom p & y = p.z;
then y = x by FUNCOP_1:7;
hence thesis by TARSKI:def 1;
end;
hence rng p = {x} by FUNCT_1:def 3;
thus thesis by ORDINAL3:15;
end;
registration
cluster non empty finite for set;
existence
proof
{the set} is finite by Lm1;
hence thesis;
end;
end;
registration
cluster empty -> finite for set;
coherence
proof
let A be set;
assume
A1: A is empty;
take {};
thus rng {} = A by A1;
thus thesis by ORDINAL1:def 11;
end;
end;
scheme OLambdaC{A()->set,C[object],F,G(object)->object}:
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))
proof
consider f being Function such that
A1: dom f = A() & for x being object st x in A() holds
(C[x] implies f.x = F(x)) & (not C[x] implies f.x = G(x))
from PARTFUN1:sch 1;
take f;
thus thesis by A1;
end;
Lm2: A is finite & B is finite implies A \/ B is finite
proof
given p be Function such that
A1: rng p = A and
A2: dom p in omega;
given q be Function such that
A3: rng q = B and
A4: dom q in omega;
reconsider domp = dom p, domq = dom q as Ordinal by A2,A4;
deffunc F(Ordinal) = p.$1;
deffunc G(Ordinal) = q.($1-^domp);
defpred P[set] means $1 in domp;
consider f such that
A5: dom f = domp+^domq and
A6: for x being Ordinal st x in domp+^domq holds
(P[x] implies f.x = F(x)) & (not P[x] implies f.x = G(x)) from OLambdaC;
take f;
reconsider domp, domq as natural Ordinal by A2,A4;
thus rng f = A \/ B
proof
thus rng f c= A \/ B
proof
let y be object;
assume y in rng f;
then consider x being object such that
A7: x in dom f and
A8: y = f.x by FUNCT_1:def 3;
reconsider x as Ordinal by A5,A7;
per cases;
suppose
A9: x in domp;
then
A10: y = p.x by A5,A6,A7,A8;
p.x in rng p by A9,FUNCT_1:def 3;
hence thesis by A1,A10,XBOOLE_0:def 3;
end;
suppose
A11: not x in domp;
then
A12: domp c= x by ORDINAL1:16;
A13: y = q.(x-^domp) by A5,A6,A7,A8,A11;
(domp)+^(x-^domp) = x by A12,ORDINAL3:def 5;
then x-^domp in dom q by A5,A7,ORDINAL3:22;
then y in B by A3,A13,FUNCT_1:def 3;
hence thesis by XBOOLE_0:def 3;
end;
end;
let x be object;
assume
A14: x in A \/ B;
per cases by A1,A3,A14,XBOOLE_0:def 3;
suppose x in rng p;
then consider y being object such that
A15: y in dom p and
A16: x = p.y by FUNCT_1:def 3;
A17: dom p c= dom f by A5,ORDINAL3:24;
then x = f.y by A5,A6,A15,A16;
hence thesis by A15,A17,FUNCT_1:def 3;
end;
suppose x in rng q;
then consider y being object such that
A18: y in domq and
A19: x = q.y by FUNCT_1:def 3;
reconsider y as Ordinal by A18;
set z = domp +^ y;
domp c= z by ORDINAL3:24;
then
A20: not z in domp by ORDINAL1:5;
A21: z in dom f by A5,A18,ORDINAL3:17;
x = q.(z-^domp) by A19,ORDINAL3:52
.= f.z by A5,A6,A20,A21;
hence thesis by A21,FUNCT_1:def 3;
end;
end;
domp+^domq is natural;
hence thesis by A5;
end;
registration
let x be object;
cluster {x} -> finite;
coherence by Lm1;
end;
registration
let x,y be object;
cluster {x,y} -> finite;
coherence
proof
{x,y} = {x} \/ {y} by ENUMSET1:1;
hence thesis by Lm2;
end;
end;
registration
let x,y,z be object;
cluster {x,y,z} -> finite;
coherence
proof
{x,y,z} = {x} \/ {y,z} by ENUMSET1:2;
hence thesis by Lm2;
end;
end;
registration
let x1,x2,x3,x4 be object;
cluster {x1,x2,x3,x4} -> finite;
coherence
proof
{x1,x2,x3,x4} = {x1} \/ {x2,x3,x4} by ENUMSET1:4;
hence thesis by Lm2;
end;
end;
registration
let x1,x2,x3,x4,x5 be object;
cluster {x1,x2,x3,x4,x5} -> finite;
coherence
proof
{x1,x2,x3,x4,x5} = {x1} \/ {x2,x3,x4,x5} by ENUMSET1:7;
hence thesis by Lm2;
end;
end;
registration
let x1,x2,x3,x4,x5,x6 be object;
cluster {x1,x2,x3,x4,x5,x6} -> finite;
coherence
proof
{x1,x2,x3,x4,x5,x6} = {x1} \/ {x2,x3,x4,x5,x6} by ENUMSET1:11;
hence thesis by Lm2;
end;
end;
registration
let x1,x2,x3,x4,x5,x6,x7 be object;
cluster {x1,x2,x3,x4,x5,x6,x7} -> finite;
coherence
proof
{x1,x2,x3,x4,x5,x6,x7} = {x1} \/ {x2,x3,x4,x5,x6,x7} by ENUMSET1:16;
hence thesis by Lm2;
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
proof
{x1,x2,x3,x4,x5,x6,x7,x8} = {x1} \/ {x2,x3,x4,x5,x6,x7,x8} by ENUMSET1:22;
hence thesis by Lm2;
end;
end;
registration
let B be finite set;
cluster -> finite for Subset of B;
coherence
proof
let A be Subset of B;
per cases;
suppose A is empty;
hence thesis;
end;
suppose A is non empty;
then consider x1 be object such that
A1: x1 in A;
consider p be Function such that
A2: rng p = B and
A3: dom p in omega by Def1;
deffunc F(object) = p.$1;
deffunc G(object) = x1;
defpred P[object] means p.$1 in A;
consider q be Function such that
A4: dom q = dom p and
A5: for x being object st x in dom p holds (P[x] implies q.x = F(x)) &
(not P[x] implies q.x = G(x)) from PARTFUN1:sch 1;
now
let y be object;
thus y in A implies ex x being object st x in dom q & y = q.x
proof
assume
A6: y in A;
then consider x being object such that
A7: x in dom p and
A8: p.x = y by A2,FUNCT_1:def 3;
take x;
thus x in dom q by A4,A7;
thus thesis by A5,A6,A7,A8;
end;
given x being object such that
A9: x in dom q and
A10: y = q.x;
per cases;
suppose p.x in A;
hence y in A by A4,A5,A9,A10;
end;
suppose not p.x in A;
hence y in A by A1,A4,A5,A9,A10;
end;
end;
then rng q = A by FUNCT_1:def 3;
hence thesis by A3,A4;
end;
end;
end;
registration
let X,Y be finite set;
cluster X \/ Y -> finite;
coherence by Lm2;
end;
theorem
A c= B & B is finite implies A is finite;
theorem
A is finite & B is finite implies A \/ B is finite;
registration
let A be set, B be finite set;
cluster A /\ B -> finite;
coherence
proof
A /\ B c= B by XBOOLE_1:17;
hence thesis;
end;
end;
registration
let A be finite set, B be set;
cluster A /\ B -> finite;
coherence;
cluster A \ B -> finite;
coherence;
end;
theorem
A is finite implies A /\ B is finite;
theorem
A is finite implies A \ B is finite;
registration
let f be Function, A be finite set;
cluster f.:A -> finite;
coherence
proof
set B = dom f /\ A;
consider p be Function such that
A1: rng p=B and
A2: dom p in omega by Def1;
take f*p;
rng (f*p) = f.:B by A1,RELAT_1:127;
hence rng (f*p) = f.:A by RELAT_1:112;
thus thesis by A1,A2,RELAT_1:27,XBOOLE_1:17;
end;
end;
theorem
A is finite implies f.:A is finite;
reserve O for Ordinal;
theorem Th6:
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
proof
assume
A1: A is finite;
let X be Subset-Family of A such that
A2: X <> {};
consider p be Function such that
A3: rng p = A and
A4: dom p in omega by A1;
defpred P[set] means p.:$1 in X;
consider G being set such that
A5: for x holds x in G iff x in bool dom p & P[x] from XFAMILY:sch 1;
G c= bool dom p
by A5;
then reconsider GX=G as Subset-Family of dom p;
set x = the Element of X;
x is Subset of A by A2,TARSKI:def 3;
then
A6: p.:(p"x) = x by A3,FUNCT_1:77;
p"x c= dom p by RELAT_1:132;
then
A7: GX <> {} by A2,A5,A6;
defpred P[set] means
$1 in omega implies for X being Subset-Family of $1 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;
A8: P[0]
proof
assume 0 in omega;
let X be Subset-Family of 0;
assume X <> {};
then
A9: X = {{}} by ZFMISC_1:1,33;
take {};
thus thesis by A9,TARSKI:def 1;
end;
A10: P[O] implies P[succ O]
proof
assume
A11: O in omega implies for X being Subset-Family of O 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;
thus succ O in omega implies
for X being Subset-Family of succ O 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
proof
assume succ O in omega;
then
A12: succ O c= omega by ORDINAL1:def 2;
let X be Subset-Family of succ O such that
A13: X <> {};
defpred P[set] means ex A st A in X & $1 = A \ {O};
consider X1 being set such that
A14: for x holds x in X1 iff x in bool O & P[x] from XFAMILY:sch 1;
X1 c= bool O
by A14;
then reconsider X2=X1 as Subset-Family of O;
set y = the Element of X;
y is Subset of succ O by A13,TARSKI:def 3;
then y \ {O} c= (O \/ {O}) \ {O} by XBOOLE_1:33;
then
A15: y \ {O} c= O \ {O} by XBOOLE_1:40;
A16: O in succ O by ORDINAL1:6;
A17: not O in O;
then y \ {O} c= O by A15,ZFMISC_1:57;
then X2 <> {} by A13,A14;
then consider Z such that
A18: Z in X2 and
A19: for B being set st B in X2 holds Z c= B implies B = Z by A11,A12,A16;
consider X1 being set such that
A20: X1 in X and
A21: Z=X1 \ {O} by A14,A18;
A22: O in {O} by TARSKI:def 1;
then
A23: not O in Z by A21,XBOOLE_0:def 5;
A24: now
assume
A25: Z \/ {O} in X;
take A=Z \/ {O};
for B being set st B in X holds A c= B implies B = A
proof
let B such that
A26: B in X;
assume
A27: A c= B;
A28: now
assume
A29: O in B;
set Y = B \ {O};
{O} c= B by A29,ZFMISC_1:31;
then
A30: B = Y \/ {O} by XBOOLE_1:45;
A \ {O} c= Y by A27,XBOOLE_1:33;
then
A31: Z \ {O} c= Y by XBOOLE_1:40;
not O in Z by A21,A22,XBOOLE_0:def 5;
then
A32: Z c= Y by A31,ZFMISC_1:57;
Y c= (O \/ {O}) \ {O} by A26,XBOOLE_1:33;
then Y c= O \ {O} by XBOOLE_1:40;
then Y c= O by A17,ZFMISC_1:57;
then Y in X2 by A14,A26;
hence thesis by A19,A30,A32;
end;
now
assume
A33: not O in B;
O in {O} by TARSKI:def 1;
then O in A by XBOOLE_0:def 3;
hence contradiction by A27,A33;
end;
hence thesis by A28;
end;
hence thesis by A25;
end;
now
assume
A34: not Z \/ {O} in X;
take A=Z;
now
assume O in X1;
then X1 = X1 \/ {O} by ZFMISC_1:40
.= Z \/ {O} by A21,XBOOLE_1:39;
hence contradiction by A20,A34;
end;
then
A35: A in X by A20,A21,ZFMISC_1:57;
for B being set st B in X holds A c= B implies B = A
proof
let B;
assume
A36: B in X;
then B \ {O} c= (O \/ {O}) \ {O} by XBOOLE_1:33;
then B \ {O} c= O \ {O} by XBOOLE_1:40;
then B \ {O} c= O by A17,ZFMISC_1:57;
then
A37: B \ {O} in X2 by A14,A36;
assume
A38: A c= B;
then A \ {O} c= B \ {O} by XBOOLE_1:33;
then
A39: A c= B \ {O} by A23,ZFMISC_1:57;
A40: now
assume
A41: O in B;
A \/ {O} = (B \ {O}) \/ {O} by A19,A37,A39
.= B \/ {O} by XBOOLE_1:39
.= B by A41,ZFMISC_1:40;
hence contradiction by A34,A36;
end;
A42: B c= O
proof
let x be object such that
A43: x in B;
x in O or x in {O} by A36,A43,XBOOLE_0:def 3;
hence thesis by A40,A43,TARSKI:def 1;
end;
B \ {O} = B by A40,ZFMISC_1:57;
then B in X2 by A14,A36,A42;
hence thesis by A19,A38;
end;
hence thesis by A35;
end;
hence thesis by A24;
end;
end;
A44: O <> 0 & O is limit_ordinal & (for B being Ordinal st B in O holds P[B])
implies P[O]
proof
assume that
A45: O <> 0 and
A46: O is limit_ordinal and for B being Ordinal st B in O holds P[B] and
A47: O in omega;
{} in O by A45,ORDINAL1:14;
then omega c= O by A46,ORDINAL1:def 11;
then O in O by A47;
hence thesis;
end;
P[O] from ORDINAL2:sch 1(A8,A10,A44);
then consider g being set such that
A48: g in GX and
A49: for B being set st B in GX holds g c= B implies B=g by A4,A7;
take p.:g;
for B st B in X holds p.:g c= B implies B = p.:g
proof
let B;
assume
A50: B in X;
assume p.:g c= B;
then
A51: p"(p.:g) c= p"B by RELAT_1:143;
A52: g c= p"(p.:g) by A48,FUNCT_1:76;
A53: p.:(p"B) = B by A3,A50,FUNCT_1:77;
p"B c= dom p by RELAT_1:132;
then p"B in GX by A5,A50,A53;
hence thesis by A49,A51,A52,A53,XBOOLE_1:1;
end;
hence thesis by A5,A48;
end;
scheme Finite{A()->set,P[set]} : P[A()]
provided
A1: A() is finite and
A2: P[{}] and
A3: for x,B being set st x in A() & B c= A() & P[B] holds P[B \/ {x}]
proof
now
assume A() <> {};
defpred R[set] means ex B st B=$1 & P[B];
consider G being set such that
A4: for x holds x in G iff x in bool A() & R[x] from XFAMILY:sch 1;
G c= bool A()
by A4;
then reconsider GA=G as Subset-Family of A();
{} c= A();
then GA <> {} by A2,A4;
then consider B such that
A5: B in GA and
A6: for X being set st X in GA holds B c= X implies B=X by A1,Th6;
A7: ex A st A = B & P[A] by A4,A5;
now set x = the Element of A() \ B;
assume B <> A();
then not A() c= B by A5;
then
A8: A() \ B <> {} by XBOOLE_1:37;
then
A9: x in A() by XBOOLE_0:def 5;
then
A10: P[B \/ {x}] by A3,A5,A7;
{x} c= A() by A9,ZFMISC_1:31;
then B \/ {x} c= A() by A5,XBOOLE_1:8;
then
A11: B \/ {x} in GA by A4,A10;
not x in B by A8,XBOOLE_0:def 5;
then not {x} c= B by ZFMISC_1:31;
then B \/ {x} <> B by XBOOLE_1:7;
hence contradiction by A6,A11,XBOOLE_1:7;
end;
hence thesis by A7;
end;
hence thesis by A2;
end;
Lm3: A
is finite & (for X st X in A holds X is finite) implies union A is finite
proof
assume that
A1: A is finite and
A2: for X st X in A holds X is finite;
defpred P[set] means ex B st B=$1 & union B is finite;
consider G being set such that
A3: for x holds x in G iff x in bool A & P[x] from XFAMILY:sch 1;
defpred P[set] means $1 in G;
{} c= A;
then
A4: P[{}] by A3,ZFMISC_1:2;
A5: for x,B being set st x in A & B c= A & P[B] holds P[B \/ {x}]
proof
let x,B be set;
assume that
A6: x in A and B c= A and
A7: B in G;
A8: ex X st X=B & union X is finite by A3,A7;
A9: x is finite by A2,A6;
A10: union (B \/ {x}) = union B \/ union {x} by ZFMISC_1:78
.= union B \/ x by ZFMISC_1:25;
A11: {x} c= A by A6,ZFMISC_1:31;
B in bool A by A3,A7;
then B \/ {x} c= A by A11,XBOOLE_1:8;
hence thesis by A3,A8,A9,A10;
end;
P[A] from Finite(A1,A4,A5);
then ex X st X=A & union X is finite by A3;
hence thesis;
end;
registration
let A,B be finite set;
cluster [:A,B:] -> finite;
coherence
proof
A1: for y holds [:A,{y}:] is finite
proof
let y;
deffunc F(object) = [$1,y];
consider f such that
A2: dom f=A &
for x being object st x in A holds f.x=F(x) from FUNCT_1:sch 3;
for x being object holds x in rng f iff x in [:A,{y}:]
proof
let x be object;
thus x in rng f implies x in [:A,{y}:]
proof
assume x in rng f;
then consider z be object such that
A3: z in dom f and
A4: f.z = x by FUNCT_1:def 3;
x = [z,y] by A2,A3,A4;
hence thesis by A2,A3,ZFMISC_1:106;
end;
thus x in [:A,{y}:] implies x in rng f
proof
assume x in [:A,{y}:];
then consider x1,x2 be object such that
A5: x1 in A and
A6: x2 in {y} and
A7: x=[x1,x2] by ZFMISC_1:def 2;
x2=y by A6,TARSKI:def 1;
then x = f.x1 by A2,A5,A7;
hence thesis by A2,A5,FUNCT_1:def 3;
end;
end;
then rng f = [:A,{y}:] by TARSKI:2;
then f.:A=[:A,{y}:] by A2,RELAT_1:113;
hence thesis;
end;
defpred P[set] means ex y st y in B & $1 = [:A,{y}:];
consider G being set such that
A8: for x holds x in G iff x in bool [:A,B:] & P[x] from XFAMILY:sch 1;
for x being object holds x in union G iff x in [:A,B:]
proof
let x be object;
thus x in union G implies x in [:A,B:]
proof
assume x in union G;
then consider X such that
A9: x in X and
A10: X in G by TARSKI:def 4;
X in bool [:A,B:]by A8,A10;
hence thesis by A9;
end;
assume x in [:A,B:];
then consider y,z be object such that
A11: y in A and
A12: z in B and
A13: x=[y,z] by ZFMISC_1:def 2;
A14: [y,z] in [:A,{z}:] by A11,ZFMISC_1:106;
{z} c= B by A12,ZFMISC_1:31;
then [:A,{z}:] c= [:A,B:] by ZFMISC_1:95;
then [:A,{z}:] in G by A8,A12;
hence thesis by A13,A14,TARSKI:def 4;
end;
then
A15: union G = [:A,B:] by TARSKI:2;
deffunc F(object) = [:A,{$1}:];
consider g being Function such that
A16: dom g = B &
for x being object st x in B holds g.x = F(x) from FUNCT_1:sch 3;
for x being object holds x in rng g iff x in G
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
thus x in rng g implies x in G
proof
assume x in rng g;
then consider y being object such that
A17: y in dom g and
A18: g.y = x by FUNCT_1:def 3;
A19: x = [:A,{y}:] by A16,A17,A18;
{y} c= B by A16,A17,ZFMISC_1:31;
then xx c= [:A,B:] by A19,ZFMISC_1:95;
hence thesis by A8,A16,A17,A19;
end;
assume x in G;
then consider y such that
A20: y in B and
A21: x = [:A,{y}:] by A8;
x = g.y by A16,A20,A21;
hence thesis by A16,A20,FUNCT_1:def 3;
end;
then rng g = G by TARSKI:2;
then
A22: g.:B = G by A16,RELAT_1:113;
for X st X in G holds X is finite
proof
let X;
assume X in G;
then ex y st y in B & X=[:A,{y}:] by A8;
hence thesis by A1;
end;
hence thesis by A15,A22,Lm3;
end;
end;
registration
let A,B,C be finite set;
cluster [:A,B,C:] -> finite;
coherence
proof
[:[:A,B:],C:] is finite;
hence thesis by ZFMISC_1:def 3;
end;
end;
registration
let A,B,C,D be finite set;
cluster [:A,B,C,D:] -> finite;
coherence
proof
[:[:A,B,C:],D:] is finite;
hence thesis by ZFMISC_1:def 4;
end;
end;
registration
let A be finite set;
cluster bool A -> finite;
coherence
proof
A1: A is finite;
defpred P[set] means bool $1 is finite;
consider G being set such that
A2: for x holds x in G iff x in bool A & P[x] from XFAMILY:sch 1;
defpred P[set] means $1 in G;
A3: bool{} is finite by ZFMISC_1:1;
{} c= A;
then
A4: P[{}] by A3,A2;
A5: for x,B being set st x in A & B c= A & P[B] holds P[B \/ {x}]
proof
let x,B be set;
assume that
A6: x in A and B c= A and
A7: B in G;
A8: x in B implies thesis by A7,XBOOLE_1:12,ZFMISC_1:31;
now
assume
A9: not x in B;
defpred P[object,object] means ex Y st Y=$1 & $2=Y \/ {x};
A10: for y,y1,y2 be object st y in bool B & P[y,y1] & P[y,y2]
holds y1 = y2;
A11: for y being object st y in bool B ex z be object st P[y,z]
proof
let y being object such that y in bool B;
reconsider y as set by TARSKI:1;
ex Y st Y=y & y \/ {x} = Y \/ {x};
hence thesis;
end;
consider f such that
A12: dom f = bool B and
A13: for y being object st y in bool B holds P[y,f.y]
from FUNCT_1:sch 2(A10,A11);
A14: bool B is finite by A2,A7;
for y being object holds y in rng f iff y in bool(B \/ {x}) \ bool B
proof let y be object;
reconsider yy=y as set by TARSKI:1;
thus y in rng f implies y in bool(B \/ {x}) \ bool B
proof
assume y in rng f;
then consider x1 be object such that
A15: x1 in dom f and
A16: f.x1=y by FUNCT_1:def 3;
consider X1 being set such that
A17: X1=x1 and
A18: f.x1= X1 \/ {x} by A12,A13,A15;
A19: X1 \/ {x} c= B \/ {x} by A12,A15,A17,XBOOLE_1:13;
x in {x} by TARSKI:def 1;
then x in yy by A16,A18,XBOOLE_0:def 3;
then not y in bool B by A9;
hence thesis by A16,A18,A19,XBOOLE_0:def 5;
end;
assume
A20: y in bool(B \/ {x}) \ bool B;
set Z=yy \ {x};
A21: now
assume
A22: not x in yy;
yy c= B
proof
let z be object;
assume
A23: z in yy;
then not z in {x} by A22,TARSKI:def 1;
hence thesis by A20,A23,XBOOLE_0:def 3;
end;
hence contradiction by A20,XBOOLE_0:def 5;
end;
A24: Z c= B by A20,XBOOLE_1:43;
then consider X such that
A25: X=Z and
A26: f.Z = X \/ {x} by A13;
X \/ {x} = yy \/ {x} by A25,XBOOLE_1:39
.= y by A21,ZFMISC_1:40;
hence thesis by A12,A24,A26,FUNCT_1:def 3;
end;
then rng f = bool(B \/ {x}) \ bool B by TARSKI:2;
then
A27: f.:(bool B) = bool(B \/ {x}) \ bool B by A12,RELAT_1:113;
A28: bool B c= bool(B \/ {x}) by XBOOLE_1:7,ZFMISC_1:67;
A29: (bool(B \/ {x}) \ bool B) \/ bool B = bool(B \/ {x}) \/
bool B by XBOOLE_1:39
.= bool(B \/ {x}) by A28,XBOOLE_1:12;
A30: {x} c= A by A6,ZFMISC_1:31;
B in bool A by A2,A7;
then B \/ {x} c= A by A30,XBOOLE_1:8;
hence thesis by A2,A14,A27,A29;
end;
hence thesis by A8;
end;
P[A] from Finite(A1,A4,A5);
hence thesis by A2;
end;
end;
theorem Th7:
A is finite & (for X st X in A holds X is finite) iff union A is finite
proof
thus A is finite & (for X st X in A holds X is finite) implies
union A is finite by Lm3;
thus union A is finite implies
A is finite & for X st X in A holds X is finite
proof
assume
A1: union A is finite;
A c= bool union A by ZFMISC_1:82;
hence A is finite by A1;
let X;
assume X in A;
then X c= union A by ZFMISC_1:74;
hence thesis by A1;
end;
end;
theorem Th8:
dom f is finite implies rng f is finite
proof
assume dom f is finite;
then f.:(dom f) is finite;
hence thesis by RELAT_1:113;
end;
theorem
Y c= rng f & f"Y is finite implies Y is finite
proof
assume Y c= rng f;
then f.:(f"Y) = Y by FUNCT_1:77;
hence thesis;
end;
registration
let X, Y be finite set;
cluster X \+\ Y -> finite;
coherence;
end;
registration
let X be set;
cluster finite for Subset of X;
existence
proof
take IT = {}X;
thus IT is finite;
end;
end;
registration
let X be non empty set;
cluster finite non empty for Subset of X;
existence
proof
take {the Element of X};
thus thesis;
end;
end;
begin :: Addenda
:: from AMI_1
theorem Th10:
for f being Function holds dom f is finite iff f is finite
proof
let f be Function;
thus dom f is finite implies f is finite
proof
assume
A1: dom f is finite;
then
A2: rng f is finite by Th8;
f c= [:dom f, rng f:] by RELAT_1:7;
hence thesis by A1,A2;
end;
pr1(dom f,rng f).:f = dom f by FUNCT_3:79;
hence thesis;
end;
:: from ALI2
theorem
for F being set st F is finite & F <> {} & F is c=-linear
ex m being set st m in F & for C being set st C in F holds m c= C
proof
defpred P[set] means $1 <> {} implies
ex m being set st m in $1 & for C being set st C in $1 holds m c= C;
let F be set such that
A1: F is finite and
A2: F <> {} and
A3: F is c=-linear;
A4: P[{}];
A5: now
let x,B be set such that
A6: x in F and
A7: B c= F and
A8: P[B];
now per cases;
suppose
A9: not ex y being set st y in B & y c=x;
assume B \/ {x} <> {};
take m = x;
x in {x} by TARSKI:def 1;
hence m in B \/ {x} by XBOOLE_0:def 3;
let C be set;
assume C in B \/ {x};
then
A10: C in B or C in {x} by XBOOLE_0:def 3;
then C,x are_c=-comparable by A3,A6,A7,TARSKI:def 1;
then C c= x or x c= C;
hence m c= C by A9,A10,TARSKI:def 1;
end;
suppose ex y being set st y in B & y c=x;
then consider y being set such that
A11: y in B and
A12: y c=x;
assume B \/ {x} <> {};
consider m being set such that
A13: m in B and
A14: for C being set st C in B holds m c= C by A8,A11;
m c= y by A11,A14;
then
A15: m c= x by A12;
take m;
thus m in B \/ {x} by A13,XBOOLE_0:def 3;
let C be set;
assume C in B \/ {x};
then C in B or C in {x} by XBOOLE_0:def 3;
hence m c= C by A14,A15,TARSKI:def 1;
end;
end;
hence P[B \/ {x}];
end;
P[F] from Finite(A1,A4,A5);
hence thesis by A2;
end;
:: from FIN_TOPO
theorem
for F being set st F is finite & F <> {} & F is c=-linear
ex m being set st m in F & for C being set st C in F holds C c= m
proof
defpred P[set] means $1 <> {} implies
ex m being set st m in $1 & for C being set st C in $1 holds C c= m;
let F be set such that
A1: F is finite and
A2: F <> {} and
A3: F is c=-linear;
A4: P[{}];
A5: now
let x,B be set such that
A6: x in F and
A7: B c= F and
A8: P[B];
now per cases;
suppose
A9: not ex y being set st y in B & x c= y;
assume B \/ {x} <> {};
take m = x;
x in {x} by TARSKI:def 1;
hence m in B \/ {x} by XBOOLE_0:def 3;
let C be set;
assume C in B \/ {x};
then
A10: C in B or C in {x} by XBOOLE_0:def 3;
then C,x are_c=-comparable by A3,A6,A7,TARSKI:def 1;
then C c= x or x c= C;
hence C c= m by A9,A10,TARSKI:def 1;
end;
suppose ex y being set st y in B & x c= y;
then consider y being set such that
A11: y in B and
A12: x c= y;
assume B \/ {x} <> {};
consider m being set such that
A13: m in B and
A14: for C being set st C in B holds C c= m by A8,A11;
y c= m by A11,A14;
then
A15: x c= m by A12;
take m;
thus m in B \/ {x} by A13,XBOOLE_0:def 3;
let C be set;
assume C in B \/ {x};
then C in B or C in {x} by XBOOLE_0:def 3;
hence C c= m by A14,A15,TARSKI:def 1;
end;
end;
hence P[B \/ {x}];
end;
P[F] from Finite(A1,A4,A5);
hence thesis by A2;
end;
:: 2006.08.25, A.T.
definition
let R be Relation;
attr R is finite-yielding means
:Def2:
for x being set st x in rng R holds x is finite;
end;
:: from CQC_THE1, 2007.03.15, A.T.
reserve a for set;
deffunc F(object) = $1`1;
theorem
X is finite & X c= [:Y,Z:] implies
ex A,B being set st A is finite & A c= Y & B is finite & B c= Z &
X c= [:A,B:]
proof
deffunc G(object) = $1`2;
assume that
A1: X is finite and
A2: X c= [:Y,Z:];
consider f being Function such that
A3: dom f = X and
A4: for a being object st a in X holds f.a = F(a) from FUNCT_1:sch 3;
consider g being Function such that
A5: dom g = X and
A6: for a being object st a in X holds g.a = G(a) from FUNCT_1:sch 3;
take A = rng f, B = rng g;
thus A is finite by A1,A3,Th8;
thus A c= Y
proof
let a be object;
assume a in A;
then consider x being object such that
A7: x in dom f and
A8: f.x = a by FUNCT_1:def 3;
consider y,z being object such that
A9: y in Y and z in Z and
A10: x = [y,z] by A2,A3,A7,ZFMISC_1:def 2;
f.x = x`1 by A3,A4,A7
.= y by A10;
hence thesis by A8,A9;
end;
thus B is finite by A1,A5,Th8;
thus B c= Z
proof
let a be object;
assume a in B;
then consider x being object such that
A11: x in dom g and
A12: g.x = a by FUNCT_1:def 3;
consider y,z being object such that
y in Y and
A13: z in Z and
A14: x = [y,z] by A2,A5,A11,ZFMISC_1:def 2;
g.x = x`2 by A5,A6,A11
.= z by A14;
hence thesis by A12,A13;
end;
thus X c= [:A,B:]
proof
let a be object;
assume
A15: a in X;
then consider x,y being object such that
x in Y and y in Z and
A16: a=[x,y] by A2,ZFMISC_1:def 2;
A17: g.a = a`2 by A6,A15
.= y by A16;
f.a = a`1 by A4,A15
.= x by A16;
then
A18: x in A by A3,A15,FUNCT_1:def 3;
y in B by A5,A15,A17,FUNCT_1:def 3;
hence thesis by A16,A18,ZFMISC_1:87;
end;
end;
theorem
X is finite & X c= [:Y,Z:] implies
ex A being set st A is finite & A c= Y & X c= [:A,Z:]
proof
assume that
A1: X is finite and
A2: X c= [:Y,Z:];
consider f being Function such that
A3: dom f = X and
A4: for a being object st a in X holds f.a = F(a) from FUNCT_1:sch 3;
take A = rng f;
thus A is finite by A1,A3,Th8;
thus A c= Y
proof
let a be object;
assume a in A;
then consider x being object such that
A5: x in dom f and
A6: f.x = a by FUNCT_1:def 3;
consider y,z being object such that
A7: y in Y and z in Z and
A8: x = [y,z] by A2,A3,A5,ZFMISC_1:def 2;
f.x = x`1 by A3,A4,A5
.= y by A8;
hence thesis by A6,A7;
end;
thus X c= [:A,Z:]
proof
let a be object;
assume
A9: a in X;
then consider x,y being object such that
x in Y and
A10: y in Z and
A11: a=[x,y] by A2,ZFMISC_1:def 2;
f.a = a`1 by A4,A9
.= x by A11;
then x in A by A3,A9,FUNCT_1:def 3;
hence thesis by A10,A11,ZFMISC_1:87;
end;
end;
:: restored, 2007.07.22, A.T.
registration
cluster finite non empty for Function;
existence
proof
{[{},{}]} is Function;
hence thesis;
end;
end;
registration
let R be finite Relation;
cluster dom R -> finite;
coherence
proof
consider f being Function such that
A1: dom f = R and
A2: for x being object st x in R holds f.x = x`1 from FUNCT_1:sch 3;
now
let x be object;
thus x in rng f implies ex y being object st [x,y] in R
proof
assume x in rng f;
then consider a being object such that
A3: a in dom f and
A4: f.a = x by FUNCT_1:def 3;
take a`2;
A5: ex x,y being object st a = [x,y] by A1,A3,RELAT_1:def 1;
x = a`1 by A1,A2,A3,A4;
hence thesis by A1,A3,A5;
end;
given y being object such that
A6: [x,y] in R;
f.[x,y] = [x,y]`1 by A2,A6
.= x;
hence x in rng f by A1,A6,FUNCT_1:3;
end;
then rng f = dom R by XTUPLE_0:def 12;
hence thesis by A1,Th8;
end;
end;
:: from SCMFSA_4, 2007.07.22, A.T.
registration
let f be Function, g be finite Function;
cluster f*g -> finite;
coherence
proof dom(f*g) c= dom g by RELAT_1:25;
hence thesis by Th10;
end;
end;
:: from SF_MASTR, 2007.07.25, A.T.
registration
let A be finite set, B be set;
cluster -> finite for Function of A, B;
coherence
proof
let f be Function of A, B;
dom f is finite;
hence thesis by Th10;
end;
end;
:: from GLIB_000, 2007.10.24, A.T.
registration
let x,y be object;
cluster x .--> y -> finite;
coherence;
end;
:: from FINSEQ_1, 2008.02.19, A.T.
registration
let R be finite Relation;
cluster rng R -> finite;
coherence
proof
consider f being Function such that
A1: dom f = R and
A2: for x being object st x in R holds f.x = x`2 from FUNCT_1:sch 3;
now
let y be object;
thus y in rng f implies ex x being object st [x,y] in R
proof
assume y in rng f;
then consider a being object such that
A3: a in dom f and
A4: f.a = y by FUNCT_1:def 3;
take a`1;
A5: ex x,y being object st a = [x,y] by A1,A3,RELAT_1:def 1;
y = a`2 by A1,A2,A3,A4;
hence thesis by A1,A3,A5;
end;
given x being object such that
A6: [x,y] in R;
f.[x,y] = [x,y]`2 by A2,A6
.= y;
hence y in rng f by A1,A6,FUNCT_1:3;
end;
then rng f = rng R by XTUPLE_0:def 13;
hence thesis by A1,Th8;
end;
end;
:: from FINSEQ_1, 2008.05.06, A.T.
registration
let f be finite Function, x be set;
cluster f"x -> finite;
coherence
proof
f"x c= dom f by RELAT_1:132;
hence thesis;
end;
end;
registration
let f, g be finite Function;
cluster f +* g -> finite;
coherence
proof
dom (f+*g) = dom f \/ dom g by FUNCT_4:def 1;
hence thesis by Th10;
end;
end;
:: from COMPTS_1, 2008.07.16, A.T
definition
let F be set;
attr F is centered means
F <> {} &
for G being set st G <> {} & G c= F & G is finite holds meet G <> {};
end;
definition
let f be Function;
redefine attr f is finite-yielding means :: redefines finite-yielding (FINSET_1, definition)
:Def4: for i being object st i in dom f holds f.i is finite;
compatibility
proof
hereby
assume
A1: f is finite-yielding;
let i be object such that i in dom f;
per cases;
suppose i in dom f;
then f.i in rng f by FUNCT_1:3;
hence f.i is finite by A1;
end;
suppose not i in dom f;
hence f.i is finite by FUNCT_1:def 2;
end;
end;
assume
A2: for i being object st i in dom f holds f.i is finite;
let i be set;
assume i in rng f;
then ex x being object st x in dom f & i = f.x by FUNCT_1:def 3;
hence thesis by A2;
end;
end;
:: from PRE_CIRC, 2009.03.04, A.T.
definition
let I be set;
let IT be I-defined Function;
redefine attr IT is finite-yielding means :: redefines finite-yielding (FINSET_1, redefinition) → finite-yielding (FINSET_1, definition)
for i being object st i in I holds IT.i is finite;
compatibility
proof
hereby
assume
A1: IT is finite-yielding;
let i be object such that i in I;
per cases;
suppose i in dom IT;
hence IT.i is finite by A1;
end;
suppose not i in dom IT;
hence IT.i is finite by FUNCT_1:def 2;
end;
end;
assume
A2: for i being object st i in I holds IT.i is finite;
let i be object;
dom IT c= I;
hence thesis by A2;
end;
end;
:: new, 2009.08.26, A.T
theorem
B is infinite implies not B in [:A,B:]
proof assume that
A1: B is infinite and
A2: B in [:A,B:];
ex x being object st x in A & B = [x,{x}] by A2,ZFMISC_1:129;
hence thesis by A1;
end;
:: new, 2009.09.30, A.T.
registration
let I be set, f be I-defined Function;
cluster finite I-defined f-compatible for Function;
existence
proof
take {};
thus thesis by FUNCT_1:104,RELAT_1:171;
end;
end;
registration
let X,Y be set;
cluster finite X-defined Y-valued for Function;
existence
proof
take {};
thus thesis by RELAT_1:171;
end;
end;
registration
let X,Y be non empty set;
cluster X-defined Y-valued non empty finite for Function;
existence
proof set x = the Element of X, y = the Element of Y;
take F = x .--> y;
thus F is X-defined;
thus F is Y-valued;
thus thesis;
end;
end;
registration
let A be set, F be finite Relation;
cluster A|`F -> finite;
coherence
proof
A|`F c= F by RELAT_1:86;
hence thesis;
end;
end;
registration
let A be set, F be finite Relation;
cluster F|A -> finite;
coherence
proof
F|A c= F by RELAT_1:59;
hence thesis;
end;
end;
registration
let A be finite set, F be Function;
cluster F|A -> finite;
coherence
proof
dom(F|A) c= A by RELAT_1:58;
hence thesis by Th10;
end;
end;
registration
let R be finite Relation;
cluster field R -> finite;
coherence;
end;
registration
cluster trivial -> finite for set;
coherence
proof
let S be set such that
A1: S is trivial;
per cases by A1,ZFMISC_1:131;
suppose S is empty;
hence thesis;
end;
suppose
ex x being object st S = {x};
hence thesis;
end;
end;
end;
registration
cluster infinite -> non trivial for set;
coherence;
end;
registration
let X be non trivial set;
cluster finite non trivial for Subset of X;
existence
proof
consider a1,a2 being object such that
A1: a1 in X & a2 in X & a1 <> a2 by ZFMISC_1:def 10;
reconsider A = {a1,a2} as Subset of X by A1,ZFMISC_1:32;
take A;
thus A is finite;
a1 in A & a2 in A by TARSKI:def 2;
hence thesis by A1,ZFMISC_1:def 10;
end;
end;
:: 2011.04.07, A.T,
registration
let x,y,a,b be object;
cluster (x,y) --> (a,b) -> finite;
coherence;
end;
:: from MATROID0, 2011.07.25, A.T.
definition
let A be set;
attr A is finite-membered means
:Def6: for B being set st B in A holds B is finite;
end;
registration
cluster empty -> finite-membered for set;
coherence;
end;
registration
let A be finite-membered set;
cluster -> finite for Element of A;
coherence
proof let B be Element of A;
per cases;
suppose A is empty;
hence thesis by SUBSET_1:def 1;
end;
suppose A is not empty;
hence thesis by Def6;
end;
end;
end;
registration
cluster non empty finite finite-membered for set;
existence
proof
take x = {{{}}};
thus x is non empty finite;
let y be set;
thus thesis by TARSKI:def 1;
end;
end;
:: from SIMPLEX0, 2011.07.25, A.T.
registration
let X be finite set;
cluster {X} -> finite-membered;
coherence
by TARSKI:def 1;
cluster bool X -> finite-membered;
coherence;
let Y be finite set;
cluster {X,Y} -> finite-membered;
coherence
by TARSKI:def 2;
end;
registration
let X be finite-membered set;
cluster -> finite-membered for Subset of X;
coherence;
let Y be finite-membered set;
cluster X \/ Y -> finite-membered;
coherence
proof
let x be set;
assume x in X\/Y;
then x in X or x in Y by XBOOLE_0:def 3;
hence thesis;
end;
end;
registration
let X be finite finite-membered set;
cluster union X -> finite;
coherence
proof
for x st x in X holds x is finite;
hence thesis by Th7;
end;
end;
registration
cluster non empty finite-yielding for Function;
existence
proof
take F = {{}} .--> {{}};
thus F is non empty;
let x be object;
assume x in {{{}}};
then x = {{}} by TARSKI:def 1;
hence F.x is finite by FUNCOP_1:72;
end;
cluster empty -> finite-yielding for Relation;
coherence;
end;
registration
let F be finite-yielding Function, x be object;
cluster F.x -> finite;
coherence
proof
per cases;
suppose x in dom F;
hence thesis by Def4;
end;
suppose not x in dom F;
hence thesis by FUNCT_1:def 2;
end;
end;
end;
registration let F be finite-yielding Relation;
cluster rng F -> finite-membered;
coherence
by Def2;
end;