:: Boolean Domains
:: by Andrzej Trybulec and Agata Darmochwa\l
::
:: Received April 14, 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 XBOOLE_0, SUBSET_1, ZFMISC_1, TARSKI, FINSET_1, FINSUB_1,
MATRIX_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FINSET_1;
constructors TARSKI, SUBSET_1, FINSET_1;
registrations XBOOLE_0, SUBSET_1, FINSET_1;
requirements SUBSET, BOOLE;
definitions TARSKI, XBOOLE_0;
equalities XBOOLE_0;
expansions TARSKI, XBOOLE_0;
theorems TARSKI, ZFMISC_1, XBOOLE_0, XBOOLE_1;
schemes XBOOLE_0;
begin :: Auxiliary theorems
reserve X,Y,x for set;
definition
let IT be set;
attr IT is cup-closed means
:Def1:
for X,Y being set st X in IT & Y in IT holds X \/ Y in IT;
attr IT is cap-closed means
for X,Y being set st X in IT & Y in IT holds X /\ Y in IT;
attr IT is diff-closed means
:Def3:
for X,Y being set st X in IT & Y in IT holds X \ Y in IT;
end;
definition
let IT be set;
attr IT is preBoolean means
IT is cup-closed diff-closed;
end;
registration
cluster preBoolean -> cup-closed diff-closed for set;
coherence;
cluster cup-closed diff-closed -> preBoolean for set;
coherence;
end;
registration
cluster non empty cup-closed cap-closed diff-closed for set;
existence
proof
take {{}};
thus {{}} is non empty;
thus {{}} is cup-closed
proof
let X,Y be set;
assume that
A1: X in {{}} and
A2: Y in {{}};
X = {} by A1,TARSKI:def 1;
hence thesis by A2;
end;
thus {{}} is cap-closed
proof
let X,Y be set;
assume that
A3: X in {{}} and
Y in {{}};
X = {} by A3,TARSKI:def 1;
hence thesis by TARSKI:def 1;
end;
thus {{}} is diff-closed
proof
let X,Y be set;
assume that
A4: X in {{}} and
Y in {{}};
X = {} by A4,TARSKI:def 1;
hence thesis by TARSKI:def 1;
end;
end;
end;
theorem Th1:
for A being set holds A is preBoolean iff for X,Y being set st X
in A & Y in A holds X \/ Y in A & X \ Y in A
proof
let A be set;
thus A is preBoolean implies for X,Y being set st X in A & Y in A holds X \/
Y in A & X \ Y in A by Def1,Def3;
assume
A1: for X,Y being set st X in A & Y in A holds X \/ Y in A & X \ Y in A;
A2: A is diff-closed
by A1;
A is cup-closed
by A1;
hence thesis by A2;
end;
reserve A for non empty preBoolean set;
definition
let A;
let X,Y be Element of A;
redefine func X \/ Y -> Element of A; :: redefines \/ (XBOOLE_0, definition)
correctness by Th1;
redefine func X \ Y -> Element of A; :: redefines \ (XBOOLE_0, definition)
correctness by Th1;
end;
theorem Th2:
X is Element of A & Y is Element of A implies X /\ Y is Element of A
proof
assume X is Element of A & Y is Element of A;
then reconsider X,Y as Element of A;
X /\ Y = X \ (X \ Y) by XBOOLE_1:48;
hence thesis;
end;
theorem Th3:
X is Element of A & Y is Element of A implies X \+\ Y is Element of A
proof
assume X is Element of A & Y is Element of A;
then reconsider X,Y as Element of A;
X \+\ Y = (X \ Y) \/ (Y \ X);
hence thesis;
end;
theorem
for A being non empty set st for X,Y being Element of A holds X \+\ Y
in A & X \ Y in A holds A is preBoolean
proof
let A be non empty set such that
A1: for X,Y being Element of A holds X \+\ Y in A & X \ Y in A;
now
let X,Y be set;
assume that
A2: X in A and
A3: Y in A;
reconsider Z = Y \ X as Element of A by A1,A2,A3;
X \/ Y = X \+\ Z by XBOOLE_1:98;
hence X \/ Y in A by A1,A2;
thus X \ Y in A by A1,A2,A3;
end;
hence thesis by Th1;
end;
theorem
for A being non empty set st for X,Y being Element of A holds X \+\ Y
in A & X /\ Y in A holds A is preBoolean
proof
let A be non empty set such that
A1: for X,Y being Element of A holds X \+\ Y in A & X /\ Y in A;
now
let X,Y be set;
assume that
A2: X in A and
A3: Y in A;
reconsider Z1 = X \+\ Y, Z2 = X /\ Y as Element of A by A1,A2,A3;
X \/ Y = Z1 \+\ Z2 by XBOOLE_1:94;
hence X \/ Y in A by A1;
X \ Y = X \+\ Z2 by XBOOLE_1:100;
hence X \ Y in A by A1,A2;
end;
hence thesis by Th1;
end;
theorem
for A being non empty set st for X,Y being Element of A holds X \+\ Y
in A & X \/ Y in A holds A is preBoolean
proof
let A be non empty set such that
A1: for X,Y being Element of A holds X \+\ Y in A & X \/ Y in A;
now
let X,Y be set;
assume that
A2: X in A and
A3: Y in A;
thus X \/ Y in A by A1,A2,A3;
reconsider Z1 = X \+\ Y, Z2 = X \/ Y as Element of A by A1,A2,A3;
X /\ Y = Z1 \+\ Z2 by XBOOLE_1:95;
then reconsider Z = X /\ Y as Element of A by A1;
X \ Y = X \+\ Z by XBOOLE_1:100;
hence X \ Y in A by A1,A2;
end;
hence thesis by Th1;
end;
definition
let A;
let X,Y be Element of A;
redefine func X /\ Y -> Element of A; :: redefines /\ (XBOOLE_0, definition)
coherence by Th2;
redefine func X \+\ Y -> Element of A; :: redefines \+\ (XBOOLE_0, definition)
coherence by Th3;
end;
theorem Th7:
{} in A
proof
set x = the Element of A;
x \ x = {} by XBOOLE_1:37;
hence thesis;
end;
theorem Th8:
for A being set holds bool A is preBoolean
proof
let A be set;
now
let X,Y be set;
assume X in bool A & Y in bool A;
then reconsider X9=X,Y9=Y as Subset of A;
X9 \/ Y9 in bool A & X9 \ Y9 in bool A;
hence X \/ Y in bool A & X \ Y in bool A;
end;
hence thesis by Th1;
end;
registration
let A be set;
cluster bool A -> preBoolean;
coherence by Th8;
end;
theorem
for A,B being non empty preBoolean set holds A /\ B is non empty preBoolean
proof
let A,B be non empty preBoolean set;
{} in A & {} in B by Th7;
then reconsider C = A /\ B as non empty set by XBOOLE_0:def 4;
now
let X,Y be set;
assume
A1: X in C & Y in C;
then
A2: X in B & Y in B by XBOOLE_0:def 4;
then
A3: X \/ Y in B by Th1;
A4: X \ Y in B by A2,Th1;
A5: X in A & Y in A by A1,XBOOLE_0:def 4;
then X \/ Y in A by Th1;
hence X \/ Y in C by A3,XBOOLE_0:def 4;
X \ Y in A by A5,Th1;
hence X \ Y in C by A4,XBOOLE_0:def 4;
end;
hence thesis by Th1;
end;
:: The set of all finite subsets of a set
definition
let A be set;
func Fin A -> preBoolean set means
:Def5:
for X being set holds X in it iff X c= A & X is finite;
existence
proof
defpred P[object] means ex y being set st y=$1 & y c= A & y is finite;
consider P being set such that
A1: for x being object holds x in P iff x in bool A & P[x]
from XBOOLE_0:sch 1;
{} c= A;
then reconsider Q=P as non empty set by A1;
for X,Y being set st X in Q & Y in Q holds X \/ Y in Q & X \ Y in Q
proof
let X,Y be set;
assume that
A2: X in Q and
A3: Y in Q;
consider Z1 being set such that
A4: Z1=X and
A5: Z1 c=A and
A6: Z1 is finite by A1,A2;
consider Z2 being set such that
A7: Z2=Y and
A8: Z2 c= A and
A9: Z2 is finite by A1,A3;
A10: Z1 \ Z2 c= A by A5;
Z1 \/ Z2 c= A by A5,A8,XBOOLE_1:8;
hence thesis by A1,A4,A6,A7,A9,A10;
end;
then reconsider R=Q as non empty preBoolean set by Th1;
for X being set holds X in R iff X c= A & X is finite
proof
let X be set;
thus X in R implies X c= A & X is finite
proof
assume X in R;
then ex Y being set st Y=X & Y c= A & Y is finite by A1;
hence thesis;
end;
thus thesis by A1;
end;
hence thesis;
end;
uniqueness
proof
let P,Q be preBoolean set;
assume that
A11: for X being set holds X in P iff X c= A & X is finite and
A12: for X being set holds X in Q iff X c= A & X is finite;
for x being object holds x in P iff x in Q
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
thus x in P implies x in Q
proof
assume x in P;
then xx c= A & xx is finite by A11;
hence thesis by A12;
end;
thus x in Q implies x in P
proof
assume x in Q;
then xx c= A & xx is finite by A12;
hence thesis by A11;
end;
end;
hence thesis by TARSKI:2;
end;
end;
registration
let A be set;
cluster Fin A -> non empty;
coherence
proof
{} c= A;
hence thesis by Def5;
end;
end;
registration
let A be set;
cluster -> finite for Element of Fin A;
coherence by Def5;
end;
theorem Th10:
for A, B being set st A c= B holds Fin A c= Fin B
proof
let A,B be set;
assume
A1: A c= B;
let X be object;
reconsider XX=X as set by TARSKI:1;
assume
A2: X in Fin A;
then XX c= A by Def5;
then XX c= B by A1;
hence X in Fin B by A2,Def5;
end;
theorem
for A, B being set holds Fin (A /\ B) = Fin A /\ Fin B
proof
let A, B be set;
Fin (A /\ B) c= Fin A & Fin (A /\ B) c= Fin B by Th10,XBOOLE_1:17;
hence Fin (A /\ B) c= Fin A /\ Fin B by XBOOLE_1:19;
let X be object;
reconsider XX=X as set by TARSKI:1;
assume
A1: X in Fin A /\ Fin B;
then X in Fin B by XBOOLE_0:def 4;
then
A2: XX c= B by Def5;
A3: X in Fin A by A1,XBOOLE_0:def 4;
then XX c= A by Def5;
then XX c= A /\ B by A2,XBOOLE_1:19;
hence X in Fin (A /\ B) by A3,Def5;
end;
theorem
for A, B being set holds Fin A \/ Fin B c= Fin (A \/ B)
proof
let A, B be set;
Fin A c= Fin (A \/ B) & Fin B c= Fin(A \/ B) by Th10,XBOOLE_1:7;
hence thesis by XBOOLE_1:8;
end;
theorem Th13:
for A being set holds Fin A c= bool A
proof
let A be set;
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in Fin A;
then xx c= A by Def5;
hence thesis;
end;
theorem Th14:
for A being set st A is finite holds Fin A = bool A
proof
let A be set;
assume
A1: A is finite;
A2: bool A c= Fin A
by A1,Def5;
Fin A c= bool A by Th13;
hence thesis by A2;
end;
theorem
Fin {} = { {} } by Th14,ZFMISC_1:1;
theorem
for A being set, X being Element of Fin A holds X is Subset of A by Def5;
theorem
for A being set, X being Subset of A st A is finite holds
X is Element of Fin A by Def5;