:: Finite Sets
:: by Agata Darmochwa\l
::
:: Received April 6, 1989
:: Copyright (c) 1990-2021 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;
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;
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;
registration
cluster non empty finite for set;
end;
registration
cluster empty -> finite for set;
end;
scheme :: FINSET_1:sch 1
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));
registration
let x be object;
cluster {x} -> finite;
end;
registration
let x,y be object;
cluster {x,y} -> finite;
end;
registration
let x,y,z be object;
cluster {x,y,z} -> finite;
end;
registration
let x1,x2,x3,x4 be object;
cluster {x1,x2,x3,x4} -> finite;
end;
registration
let x1,x2,x3,x4,x5 be object;
cluster {x1,x2,x3,x4,x5} -> finite;
end;
registration
let x1,x2,x3,x4,x5,x6 be object;
cluster {x1,x2,x3,x4,x5,x6} -> finite;
end;
registration
let x1,x2,x3,x4,x5,x6,x7 be object;
cluster {x1,x2,x3,x4,x5,x6,x7} -> finite;
end;
registration
let x1,x2,x3,x4,x5,x6,x7,x8 be object;
cluster {x1,x2,x3,x4,x5,x6,x7,x8} -> finite;
end;
registration
let B be finite set;
cluster -> finite for Subset of B;
end;
registration
let X,Y be finite set;
cluster X \/ Y -> finite;
end;
theorem :: FINSET_1:1
A c= B & B is finite implies A is finite;
theorem :: FINSET_1:2
A is finite & B is finite implies A \/ B is finite;
registration
let A be set, B be finite set;
cluster A /\ B -> finite;
end;
registration
let A be finite set, B be set;
cluster A /\ B -> finite;
cluster A \ B -> finite;
end;
theorem :: FINSET_1:3
A is finite implies A /\ B is finite;
theorem :: FINSET_1:4
A is finite implies A \ B is finite;
registration
let f be Function, A be finite set;
cluster f.:A -> finite;
end;
theorem :: FINSET_1:5
A is finite implies f.:A is finite;
reserve O for Ordinal;
theorem :: FINSET_1:6
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 :: FINSET_1:sch 2
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}];
registration
let A,B be finite set;
cluster [:A,B:] -> finite;
end;
registration
let A,B,C be finite set;
cluster [:A,B,C:] -> finite;
end;
registration
let A,B,C,D be finite set;
cluster [:A,B,C,D:] -> finite;
end;
registration
let A be finite set;
cluster bool A -> finite;
end;
theorem :: FINSET_1:7
A is finite & (for X st X in A holds X is finite) iff union A is finite;
theorem :: FINSET_1:8
dom f is finite implies rng f is finite;
theorem :: FINSET_1:9
Y c= rng f & f"Y is finite implies Y is finite;
registration
let X, Y be finite set;
cluster X \+\ Y -> finite;
end;
registration
let X be set;
cluster finite for Subset of X;
end;
registration
let X be non empty set;
cluster finite non empty for Subset of X;
end;
begin :: Addenda
:: from AMI_1
theorem :: FINSET_1:10
for f being Function holds dom f is finite iff f is finite;
:: from ALI2
theorem :: FINSET_1:11
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;
:: from FIN_TOPO
theorem :: FINSET_1:12
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;
:: 2006.08.25, A.T.
definition
let R be Relation;
attr R is finite-yielding means
:: FINSET_1:def 2
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;
theorem :: FINSET_1:13
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:];
theorem :: FINSET_1:14
X is finite & X c= [:Y,Z:] implies
ex A being set st A is finite & A c= Y & X c= [:A,Z:];
:: restored, 2007.07.22, A.T.
registration
cluster finite non empty for Function;
end;
registration
let R be finite Relation;
cluster dom R -> finite;
end;
:: from SCMFSA_4, 2007.07.22, A.T.
registration
let f be Function, g be finite Function;
cluster f*g -> finite;
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;
end;
:: from GLIB_000, 2007.10.24, A.T.
registration
let x,y be object;
cluster x .--> y -> finite;
end;
:: from FINSEQ_1, 2008.02.19, A.T.
registration
let R be finite Relation;
cluster rng R -> finite;
end;
:: from FINSEQ_1, 2008.05.06, A.T.
registration
let f be finite Function, x be set;
cluster f"x -> finite;
end;
registration
let f, g be finite Function;
cluster f +* g -> finite;
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;
definition
let f be Function;
redefine attr f is finite-yielding means
:: FINSET_1:def 4
for i being object st i in dom f holds f.i is finite;
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
:: FINSET_1:def 5
for i being object st i in I holds IT.i is finite;
end;
:: new, 2009.08.26, A.T
theorem :: FINSET_1:15
B is infinite implies not B in [:A,B:];
:: new, 2009.09.30, A.T.
registration
let I be set, f be I-defined Function;
cluster finite I-defined f-compatible for Function;
end;
registration
let X,Y be set;
cluster finite X-defined Y-valued for Function;
end;
registration
let X,Y be non empty set;
cluster X-defined Y-valued non empty finite for Function;
end;
registration
let A be set, F be finite Relation;
cluster A|`F -> finite;
end;
registration
let A be set, F be finite Relation;
cluster F|A -> finite;
end;
registration
let A be finite set, F be Function;
cluster F|A -> finite;
end;
registration
let R be finite Relation;
cluster field R -> finite;
end;
registration
cluster trivial -> finite for set;
end;
registration
cluster infinite -> non trivial for set;
end;
registration
let X be non trivial set;
cluster finite non trivial for Subset of X;
end;
:: 2011.04.07, A.T,
registration
let x,y,a,b be object;
cluster (x,y) --> (a,b) -> finite;
end;
:: from MATROID0, 2011.07.25, A.T.
definition
let A be set;
attr A is finite-membered means
:: FINSET_1:def 6
for B being set st B in A holds B is finite;
end;
registration
cluster empty -> finite-membered for set;
end;
registration
let A be finite-membered set;
cluster -> finite for Element of A;
end;
registration
cluster non empty finite finite-membered for set;
end;
:: from SIMPLEX0, 2011.07.25, A.T.
registration
let X be finite set;
cluster {X} -> finite-membered;
cluster bool X -> finite-membered;
let Y be finite set;
cluster {X,Y} -> finite-membered;
end;
registration
let X be finite-membered set;
cluster -> finite-membered for Subset of X;
let Y be finite-membered set;
cluster X \/ Y -> finite-membered;
end;
registration
let X be finite finite-membered set;
cluster union X -> finite;
end;
registration
cluster non empty finite-yielding for Function;
cluster empty -> finite-yielding for Relation;
end;
registration
let F be finite-yielding Function, x be object;
cluster F.x -> finite;
end;
registration let F be finite-yielding Relation;
cluster rng F -> finite-membered;
end;