begin
:: deftheorem BVFUNC_1:def 1 :
canceled;
:: deftheorem BVFUNC_1:def 2 :
canceled;
:: deftheorem Def3 defines <= BVFUNC_1:def 3 :
for k, l being boolean set holds
( k <= l iff k => l = TRUE );
begin
:: deftheorem BVFUNC_1:def 4 :
canceled;
:: deftheorem Def5 defines 'or' BVFUNC_1:def 5 :
for p, q, b3 being boolean-valued Function holds
( b3 = p 'or' q iff ( dom b3 = (dom p) /\ (dom q) & ( for x being set st x in dom b3 holds
b3 . x = (p . x) 'or' (q . x) ) ) );
:: deftheorem Def6 defines 'xor' BVFUNC_1:def 6 :
for p, q being boolean-valued Function
for b3 being Function holds
( b3 = p 'xor' q iff ( dom b3 = (dom p) /\ (dom q) & ( for x being set st x in dom b3 holds
b3 . x = (p . x) 'xor' (q . x) ) ) );
:: deftheorem Def7 defines 'or' BVFUNC_1:def 7 :
for A being non empty set
for p, q, b4 being Element of Funcs A,BOOLEAN holds
( b4 = p 'or' q iff for x being Element of A holds b4 . x = (p . x) 'or' (q . x) );
:: deftheorem defines 'xor' BVFUNC_1:def 8 :
for A being non empty set
for p, q, b4 being Element of Funcs A,BOOLEAN holds
( b4 = p 'xor' q iff for x being Element of A holds b4 . x = (p . x) 'xor' (q . x) );
:: deftheorem Def9 defines 'imp' BVFUNC_1:def 9 :
for p, q being boolean-valued Function
for b3 being Function holds
( b3 = p 'imp' q iff ( dom b3 = (dom p) /\ (dom q) & ( for x being set st x in dom b3 holds
b3 . x = (p . x) => (q . x) ) ) );
:: deftheorem Def10 defines 'eqv' BVFUNC_1:def 10 :
for p, q being boolean-valued Function
for b3 being Function holds
( b3 = p 'eqv' q iff ( dom b3 = (dom p) /\ (dom q) & ( for x being set st x in dom b3 holds
b3 . x = (p . x) <=> (q . x) ) ) );
:: deftheorem Def11 defines 'imp' BVFUNC_1:def 11 :
for A being non empty set
for p, q, b4 being Element of Funcs A,BOOLEAN holds
( b4 = p 'imp' q iff for x being Element of A holds b4 . x = ('not' (p . x)) 'or' (q . x) );
:: deftheorem Def12 defines 'eqv' BVFUNC_1:def 12 :
for A being non empty set
for p, q, b4 being Element of Funcs A,BOOLEAN holds
( b4 = p 'eqv' q iff for x being Element of A holds b4 . x = 'not' ((p . x) 'xor' (q . x)) );
:: deftheorem Def13 defines O_el BVFUNC_1:def 13 :
for Y being non empty set
for b2 being Element of Funcs Y,BOOLEAN holds
( b2 = O_el Y iff for x being Element of Y holds b2 . x = FALSE );
:: deftheorem Def14 defines I_el BVFUNC_1:def 14 :
for Y being non empty set
for b2 being Element of Funcs Y,BOOLEAN holds
( b2 = I_el Y iff for x being Element of Y holds b2 . x = TRUE );
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem Th5:
theorem
theorem
theorem Th8:
theorem Th9:
theorem
theorem
theorem Th12:
theorem Th13:
theorem
theorem
theorem
theorem
:: deftheorem Def15 defines '<' BVFUNC_1:def 15 :
for Y being non empty set
for a, b being Element of Funcs Y,BOOLEAN holds
( a '<' b iff for x being Element of Y st a . x = TRUE holds
b . x = TRUE );
theorem
theorem Th19:
theorem
theorem
begin
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:
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:
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 :
for Y being non empty set
for a, b3 being Element of Funcs Y,BOOLEAN holds
( ( ( for x being Element of Y holds a . x = TRUE ) implies ( b3 = B_INF a iff b3 = I_el Y ) ) & ( not for x being Element of Y holds a . x = TRUE implies ( b3 = B_INF a iff b3 = O_el Y ) ) );
:: deftheorem Def17 defines B_SUP BVFUNC_1:def 17 :
for Y being non empty set
for a, b3 being Element of Funcs Y,BOOLEAN holds
( ( ( for x being Element of Y holds a . x = FALSE ) implies ( b3 = B_SUP a iff b3 = O_el Y ) ) & ( not for x being Element of Y holds a . x = FALSE implies ( b3 = B_SUP a iff b3 = I_el Y ) ) );
theorem Th22:
theorem
theorem Th24:
theorem Th25:
theorem
theorem
theorem
theorem
theorem
begin
:: deftheorem Def18 defines is_dependent_of BVFUNC_1:def 18 :
for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for PA being a_partition of Y holds
( a is_dependent_of PA iff for F being set st F in PA holds
for x1, x2 being set st x1 in F & x2 in F holds
a . x1 = a . x2 );
theorem
theorem
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:
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 :
for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for PA being a_partition of Y
for b4 being Element of Funcs Y,BOOLEAN holds
( b4 = B_INF a,PA iff for y being Element of Y holds
( ( ( for x being Element of Y st x in EqClass y,PA holds
a . x = TRUE ) implies b4 . y = TRUE ) & ( ex x being Element of Y st
( x in EqClass y,PA & not a . x = TRUE ) implies b4 . y = FALSE ) ) );
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:
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 :
for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for PA being a_partition of Y
for b4 being Element of Funcs Y,BOOLEAN holds
( b4 = B_SUP a,PA iff for y being Element of Y holds
( ( ex x being Element of Y st
( x in EqClass y,PA & a . x = TRUE ) implies b4 . y = TRUE ) & ( ( for x being Element of Y holds
( not x in EqClass y,PA or not a . x = TRUE ) ) implies b4 . y = FALSE ) ) );
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
:: deftheorem defines GPart BVFUNC_1:def 21 :
for Y being non empty set
for f being Element of Funcs Y,BOOLEAN holds GPart f = {{ x where x is Element of Y : f . x = TRUE } ,{ x9 where x9 is Element of Y : f . x9 = FALSE } } \ {{} };
theorem
theorem