:: A Theory of Boolean Valued Functions and Partitions
:: by Shunichi Kobayashi and Kui Jia
::
:: Received October 22, 1998
:: Copyright (c) 1998 Association of Mizar Users
:: deftheorem BVFUNC_1:def 1 :
canceled;
:: deftheorem BVFUNC_1:def 2 :
canceled;
:: deftheorem Def3 defines <= BVFUNC_1:def 3 :
:: deftheorem BVFUNC_1:def 4 :
canceled;
:: deftheorem Def5 defines 'or' BVFUNC_1:def 5 :
:: deftheorem Def6 defines 'xor' BVFUNC_1:def 6 :
:: deftheorem Def7 defines 'or' BVFUNC_1:def 7 :
:: deftheorem defines 'xor' BVFUNC_1:def 8 :
:: deftheorem Def9 defines 'imp' BVFUNC_1:def 9 :
:: deftheorem Def10 defines 'eqv' BVFUNC_1:def 10 :
:: deftheorem Def11 defines 'imp' BVFUNC_1:def 11 :
:: deftheorem Def12 defines 'eqv' BVFUNC_1:def 12 :
:: deftheorem Def13 defines O_el BVFUNC_1:def 13 :
:: deftheorem Def14 defines I_el BVFUNC_1:def 14 :
theorem :: BVFUNC_1:1
canceled;
theorem :: BVFUNC_1:2
canceled;
theorem :: BVFUNC_1:3
canceled;
theorem :: BVFUNC_1:4
theorem Th5: :: BVFUNC_1:5
theorem :: BVFUNC_1:6
theorem :: BVFUNC_1:7
theorem Th8: :: BVFUNC_1:8
theorem Th9: :: BVFUNC_1:9
theorem :: BVFUNC_1:10
theorem :: BVFUNC_1:11
theorem Th12: :: BVFUNC_1:12
theorem Th13: :: BVFUNC_1:13
theorem :: BVFUNC_1:14
theorem :: BVFUNC_1:15
theorem :: BVFUNC_1:16
theorem :: BVFUNC_1:17
:: deftheorem Def15 defines '<' BVFUNC_1:def 15 :
theorem :: BVFUNC_1:18
theorem Th19: :: BVFUNC_1:19
theorem :: BVFUNC_1:20
theorem :: BVFUNC_1:21
definition
let Y be non
empty set ;
let a be
Element of
Funcs Y,
BOOLEAN ;
func B_INF a -> Element of
Funcs Y,
BOOLEAN means :
Def16:
:: BVFUNC_1:def 16
it = I_el Y if for
x being
Element of
Y holds
a . x = TRUE otherwise it = O_el Y;
correctness
consistency
for b1 being Element of Funcs Y,BOOLEAN holds verum;
existence
( ( for b1 being Element of Funcs Y,BOOLEAN holds verum ) & ( ( for x being Element of Y holds a . x = TRUE ) implies ex b1 being Element of Funcs Y,BOOLEAN st b1 = I_el Y ) & ( not for x being Element of Y holds a . x = TRUE implies ex b1 being Element of Funcs Y,BOOLEAN st b1 = O_el Y ) );
uniqueness
for b1, b2 being Element of Funcs Y,BOOLEAN holds
( ( ( for x being Element of Y holds a . x = TRUE ) & b1 = I_el Y & b2 = I_el Y implies b1 = b2 ) & ( not for x being Element of Y holds a . x = TRUE & b1 = O_el Y & b2 = O_el Y implies b1 = b2 ) );
;
func B_SUP a -> Element of
Funcs Y,
BOOLEAN means :
Def17:
:: BVFUNC_1:def 17
it = O_el Y if for
x being
Element of
Y holds
a . x = FALSE otherwise it = I_el Y;
correctness
consistency
for b1 being Element of Funcs Y,BOOLEAN holds verum;
existence
( ( for b1 being Element of Funcs Y,BOOLEAN holds verum ) & ( ( for x being Element of Y holds a . x = FALSE ) implies ex b1 being Element of Funcs Y,BOOLEAN st b1 = O_el Y ) & ( not for x being Element of Y holds a . x = FALSE implies ex b1 being Element of Funcs Y,BOOLEAN st b1 = I_el Y ) );
uniqueness
for b1, b2 being Element of Funcs Y,BOOLEAN holds
( ( ( for x being Element of Y holds a . x = FALSE ) & b1 = O_el Y & b2 = O_el Y implies b1 = b2 ) & ( not for x being Element of Y holds a . x = FALSE & b1 = I_el Y & b2 = I_el Y implies b1 = b2 ) );
;
end;
:: deftheorem Def16 defines B_INF BVFUNC_1:def 16 :
:: deftheorem Def17 defines B_SUP BVFUNC_1:def 17 :
theorem Th22: :: BVFUNC_1:22
theorem :: BVFUNC_1:23
theorem Th24: :: BVFUNC_1:24
theorem Th25: :: BVFUNC_1:25
theorem :: BVFUNC_1:26
theorem :: BVFUNC_1:27
theorem :: BVFUNC_1:28
theorem :: BVFUNC_1:29
theorem :: BVFUNC_1:30
:: deftheorem Def18 defines is_dependent_of BVFUNC_1:def 18 :
theorem :: BVFUNC_1:31
theorem :: BVFUNC_1:32
definition
let Y be non
empty set ;
let a be
Element of
Funcs Y,
BOOLEAN ;
let PA be
a_partition of
Y;
func B_INF a,
PA -> Element of
Funcs Y,
BOOLEAN means :
Def19:
:: BVFUNC_1:def 19
for
y being
Element of
Y holds
( ( ( for
x being
Element of
Y st
x in EqClass y,
PA holds
a . x = TRUE ) implies
it . y = TRUE ) & ( ex
x being
Element of
Y st
(
x in EqClass y,
PA & not
a . x = TRUE ) implies
it . y = FALSE ) );
existence
ex b1 being Element of Funcs Y,BOOLEAN st
for y being Element of Y holds
( ( ( for x being Element of Y st x in EqClass y,PA holds
a . x = TRUE ) implies b1 . y = TRUE ) & ( ex x being Element of Y st
( x in EqClass y,PA & not a . x = TRUE ) implies b1 . y = FALSE ) )
uniqueness
for b1, b2 being Element of Funcs Y,BOOLEAN st ( for y being Element of Y holds
( ( ( for x being Element of Y st x in EqClass y,PA holds
a . x = TRUE ) implies b1 . y = TRUE ) & ( ex x being Element of Y st
( x in EqClass y,PA & not a . x = TRUE ) implies b1 . y = FALSE ) ) ) & ( for y being Element of Y holds
( ( ( for x being Element of Y st x in EqClass y,PA holds
a . x = TRUE ) implies b2 . y = TRUE ) & ( ex x being Element of Y st
( x in EqClass y,PA & not a . x = TRUE ) implies b2 . y = FALSE ) ) ) holds
b1 = b2
end;
:: deftheorem Def19 defines B_INF BVFUNC_1:def 19 :
definition
let Y be non
empty set ;
let a be
Element of
Funcs Y,
BOOLEAN ;
let PA be
a_partition of
Y;
func B_SUP a,
PA -> Element of
Funcs Y,
BOOLEAN means :
Def20:
:: BVFUNC_1:def 20
for
y being
Element of
Y holds
( ( ex
x being
Element of
Y st
(
x in EqClass y,
PA &
a . x = TRUE ) implies
it . y = TRUE ) & ( ( for
x being
Element of
Y holds
( not
x in EqClass y,
PA or not
a . x = TRUE ) ) implies
it . y = FALSE ) );
existence
ex b1 being Element of Funcs Y,BOOLEAN st
for y being Element of Y holds
( ( ex x being Element of Y st
( x in EqClass y,PA & a . x = TRUE ) implies b1 . y = TRUE ) & ( ( for x being Element of Y holds
( not x in EqClass y,PA or not a . x = TRUE ) ) implies b1 . y = FALSE ) )
uniqueness
for b1, b2 being Element of Funcs Y,BOOLEAN st ( for y being Element of Y holds
( ( ex x being Element of Y st
( x in EqClass y,PA & a . x = TRUE ) implies b1 . y = TRUE ) & ( ( for x being Element of Y holds
( not x in EqClass y,PA or not a . x = TRUE ) ) implies b1 . y = FALSE ) ) ) & ( for y being Element of Y holds
( ( ex x being Element of Y st
( x in EqClass y,PA & a . x = TRUE ) implies b2 . y = TRUE ) & ( ( for x being Element of Y holds
( not x in EqClass y,PA or not a . x = TRUE ) ) implies b2 . y = FALSE ) ) ) holds
b1 = b2
end;
:: deftheorem Def20 defines B_SUP BVFUNC_1:def 20 :
theorem :: BVFUNC_1:33
theorem :: BVFUNC_1:34
theorem :: BVFUNC_1:35
theorem :: BVFUNC_1:36
theorem :: BVFUNC_1:37
theorem :: BVFUNC_1:38
theorem :: BVFUNC_1:39
theorem :: BVFUNC_1:40
theorem :: BVFUNC_1:41
theorem :: BVFUNC_1:42
theorem :: BVFUNC_1:43
:: deftheorem defines GPart BVFUNC_1:def 21 :
theorem :: BVFUNC_1:44
theorem :: BVFUNC_1:45