:: Boolean Domains
:: by Andrzej Trybulec and Agata Darmochwa\l
::
:: Received April 14, 1989
:: Copyright (c) 1990-2012 Association of Mizar Users
begin
definition
let
IT
be
set
;
attr
IT
is
cup-closed
means
:
Def1
:
:: FINSUB_1:def 1
for
X
,
Y
being
set
st
X
in
IT
&
Y
in
IT
holds
X
\/
Y
in
IT
;
attr
IT
is
cap-closed
means
:: FINSUB_1:def 2
for
X
,
Y
being
set
st
X
in
IT
&
Y
in
IT
holds
X
/\
Y
in
IT
;
attr
IT
is
diff-closed
means
:
Def3
:
:: FINSUB_1:def 3
for
X
,
Y
being
set
st
X
in
IT
&
Y
in
IT
holds
X
\
Y
in
IT
;
end;
::
deftheorem
Def1
defines
cup-closed
FINSUB_1:def 1 :
for
IT
being
set
holds
(
IT
is
cup-closed
iff for
X
,
Y
being
set
st
X
in
IT
&
Y
in
IT
holds
X
\/
Y
in
IT
);
::
deftheorem
defines
cap-closed
FINSUB_1:def 2 :
for
IT
being
set
holds
(
IT
is
cap-closed
iff for
X
,
Y
being
set
st
X
in
IT
&
Y
in
IT
holds
X
/\
Y
in
IT
);
::
deftheorem
Def3
defines
diff-closed
FINSUB_1:def 3 :
for
IT
being
set
holds
(
IT
is
diff-closed
iff for
X
,
Y
being
set
st
X
in
IT
&
Y
in
IT
holds
X
\
Y
in
IT
);
definition
let
IT
be
set
;
attr
IT
is
preBoolean
means
:
Def4
:
:: FINSUB_1:def 4
(
IT
is
cup-closed
&
IT
is
diff-closed
);
end;
::
deftheorem
Def4
defines
preBoolean
FINSUB_1:def 4 :
for
IT
being
set
holds
(
IT
is
preBoolean
iff (
IT
is
cup-closed
&
IT
is
diff-closed
) );
registration
cluster
preBoolean
->
cup-closed
diff-closed
for
set
;
coherence
for
b
1
being
set
st
b
1
is
preBoolean
holds
(
b
1
is
cup-closed
&
b
1
is
diff-closed
)
by
Def4
;
cluster
cup-closed
diff-closed
->
preBoolean
for
set
;
coherence
for
b
1
being
set
st
b
1
is
cup-closed
&
b
1
is
diff-closed
holds
b
1
is
preBoolean
by
Def4
;
end;
registration
cluster
non
empty
cup-closed
cap-closed
diff-closed
for
set
;
existence
ex
b
1
being
set
st
( not
b
1
is
empty
&
b
1
is
cup-closed
&
b
1
is
cap-closed
&
b
1
is
diff-closed
)
proof
end;
end;
theorem
Th1
:
:: FINSUB_1:1
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
end;
definition
let
A
be non
empty
preBoolean
set
;
let
X
,
Y
be
Element
of
A
;
:: original:
\/
redefine
func
X
\/
Y
->
Element
of
A
;
correctness
coherence
X
\/
Y
is
Element
of
A
;
by
Th1
;
:: original:
\
redefine
func
X
\
Y
->
Element
of
A
;
correctness
coherence
X
\
Y
is
Element
of
A
;
by
Th1
;
end;
theorem
Th2
:
:: FINSUB_1:2
for
X
,
Y
being
set
for
A
being non
empty
preBoolean
set
st
X
is
Element
of
A
&
Y
is
Element
of
A
holds
X
/\
Y
is
Element
of
A
proof
end;
theorem
Th3
:
:: FINSUB_1:3
for
X
,
Y
being
set
for
A
being non
empty
preBoolean
set
st
X
is
Element
of
A
&
Y
is
Element
of
A
holds
X
\+\
Y
is
Element
of
A
proof
end;
theorem
:: FINSUB_1:4
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
end;
theorem
:: FINSUB_1:5
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
end;
theorem
:: FINSUB_1:6
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
end;
definition
let
A
be non
empty
preBoolean
set
;
let
X
,
Y
be
Element
of
A
;
:: original:
/\
redefine
func
X
/\
Y
->
Element
of
A
;
coherence
X
/\
Y
is
Element
of
A
by
Th2
;
:: original:
\+\
redefine
func
X
\+\
Y
->
Element
of
A
;
coherence
X
\+\
Y
is
Element
of
A
by
Th3
;
end;
theorem
Th7
:
:: FINSUB_1:7
for
A
being non
empty
preBoolean
set
holds
{}
in
A
proof
end;
theorem
Th8
:
:: FINSUB_1:8
for
A
being
set
holds
bool
A
is
preBoolean
proof
end;
registration
let
A
be
set
;
cluster
bool
A
->
preBoolean
;
coherence
bool
A
is
preBoolean
by
Th8
;
end;
theorem
:: FINSUB_1:9
for
A
,
B
being non
empty
preBoolean
set
holds
( not
A
/\
B
is
empty
&
A
/\
B
is
preBoolean
)
proof
end;
:: The set of all finite subsets of a set
definition
let
A
be
set
;
func
Fin
A
->
preBoolean
set
means
:
Def5
:
:: FINSUB_1:def 5
for
X
being
set
holds
(
X
in
it
iff (
X
c=
A
&
X
is
finite
) );
existence
ex
b
1
being
preBoolean
set
st
for
X
being
set
holds
(
X
in
b
1
iff (
X
c=
A
&
X
is
finite
) )
proof
end;
uniqueness
for
b
1
,
b
2
being
preBoolean
set
st ( for
X
being
set
holds
(
X
in
b
1
iff (
X
c=
A
&
X
is
finite
) ) ) & ( for
X
being
set
holds
(
X
in
b
2
iff (
X
c=
A
&
X
is
finite
) ) ) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def5
defines
Fin
FINSUB_1:def 5 :
for
A
being
set
for
b
2
being
preBoolean
set
holds
(
b
2
=
Fin
A
iff for
X
being
set
holds
(
X
in
b
2
iff (
X
c=
A
&
X
is
finite
) ) );
registration
let
A
be
set
;
cluster
Fin
A
->
non
empty
preBoolean
;
coherence
not
Fin
A
is
empty
proof
end;
end;
registration
let
A
be
set
;
cluster
->
finite
for
Element
of
Fin
A
;
coherence
for
b
1
being
Element
of
Fin
A
holds
b
1
is
finite
by
Def5
;
end;
theorem
Th10
:
:: FINSUB_1:10
for
A
,
B
being
set
st
A
c=
B
holds
Fin
A
c=
Fin
B
proof
end;
theorem
:: FINSUB_1:11
for
A
,
B
being
set
holds
Fin
(
A
/\
B
)
=
(
Fin
A
)
/\
(
Fin
B
)
proof
end;
theorem
:: FINSUB_1:12
for
A
,
B
being
set
holds
(
Fin
A
)
\/
(
Fin
B
)
c=
Fin
(
A
\/
B
)
proof
end;
theorem
Th13
:
:: FINSUB_1:13
for
A
being
set
holds
Fin
A
c=
bool
A
proof
end;
theorem
Th14
:
:: FINSUB_1:14
for
A
being
set
st
A
is
finite
holds
Fin
A
=
bool
A
proof
end;
theorem
:: FINSUB_1:15
Fin
{}
=
{
{}
}
by
Th14
,
ZFMISC_1:1
;
:: Finite subsets
definition
let
A
be
set
;
mode
Finite_Subset of
A
is
Element
of
Fin
A
;
end;
theorem
:: FINSUB_1:16
for
A
being
set
for
X
being
Finite_Subset
of
A
holds
X
is
finite
;
theorem
:: FINSUB_1:17
for
A
being
set
for
X
being
Finite_Subset
of
A
holds
X
is
Subset
of
A
by
Def5
;
theorem
:: FINSUB_1:18
for
A
being
set
for
X
being
Subset
of
A
st
A
is
finite
holds
X
is
Finite_Subset
of
A
by
Def5
;