:: BVFUNC_2 semantic presentation
theorem Th1: :: BVFUNC_2:1
definition
let c
1 be non
empty set ;
let c
2 be
Subset of
(PARTITIONS c1);
func '/\' c
2 -> a_partition of a
1 means :
Def1:
:: BVFUNC_2:def 1
for b
1 being
set holds
( b
1 in a
3 iff ex b
2 being
Functionex b
3 being
Subset-Family of a
1 st
(
dom b
2 = a
2 &
rng b
2 = b
3 & ( for b
4 being
set holds
( b
4 in a
2 implies b
2 . b
4 in b
4 ) ) & b
1 = Intersect b
3 & b
1 <> {} ) );
existence
ex b1 being a_partition of c1 st
for b2 being set holds
( b2 in b1 iff ex b3 being Functionex b4 being Subset-Family of c1 st
( dom b3 = c2 & rng b3 = b4 & ( for b5 being set holds
( b5 in c2 implies b3 . b5 in b5 ) ) & b2 = Intersect b4 & b2 <> {} ) )
proof
defpred S
1[
set ] means ex b
1 being
Functionex b
2 being
Subset-Family of c
1 st
(
dom b
1 = c
2 &
rng b
1 = b
2 & ( for b
3 being
set holds
( b
3 in c
2 implies b
1 . b
3 in b
3 ) ) & a
1 = Intersect b
2 & a
1 <> {} );
consider c
3 being
set such that E2:
for b
1 being
set holds
( b
1 in c
3 iff ( b
1 in bool c
1 & S
1[b
1] ) )
from XBOOLE_0:sch 1();
take
c
3
;
E3:
union c
3 = c
1
E4:
for b
1 being
Subset of c
1 holds
( b
1 in c
3 implies ( b
1 <> {} & ( for b
2 being
Subset of c
1 holds
not ( b
2 in c
3 & not b
1 = b
2 & not b
1 misses b
2 ) ) ) )
proof
let c
4 be
Subset of c
1;
assume
c
4 in c
3
;
then consider c
5 being
Function, c
6 being
Subset-Family of c
1 such that E5:
(
dom c
5 = c
2 &
rng c
5 = c
6 & ( for b
1 being
set holds
( b
1 in c
2 implies c
5 . b
1 in b
1 ) ) & c
4 = Intersect c
6 & c
4 <> {} )
by E2;
thus
c
4 <> {}
by E5;
let c
7 be
Subset of c
1;
assume
c
7 in c
3
;
then consider c
8 being
Function, c
9 being
Subset-Family of c
1 such that E6:
(
dom c
8 = c
2 &
rng c
8 = c
9 & ( for b
1 being
set holds
( b
1 in c
2 implies c
8 . b
1 in b
1 ) ) & c
7 = Intersect c
9 & c
7 <> {} )
by E2;
per cases
not ( not c2 = {} & not c2 <> {} )
;
suppose
c
2 <> {}
;
then E7:
(
rng c
5 <> {} &
rng c
8 <> {} )
by E5, E6, RELAT_1:65;
now
assume
c
4 meets c
7
;
then consider c
10 being
set such that E8:
( c
10 in c
4 & c
10 in c
7 )
by XBOOLE_0:3;
E9:
c
10 in meet (rng c5)
by E5, E7, E8, SETFAM_1:def 10;
E10:
c
10 in meet (rng c8)
by E6, E7, E8, SETFAM_1:def 10;
for b
1 being
set holds
( b
1 in c
2 implies c
5 . b
1 = c
8 . b
1 )
proof
let c
11 be
set ;
assume E11:
c
11 in c
2
;
then reconsider c
12 = c
11 as
a_partition of c
1 by PARTIT1:def 3;
E12:
c
5 . c
12 in c
12
by E5, E11;
E13:
c
8 . c
12 in c
12
by E6, E11;
E14:
c
5 . c
12 in rng c
5
by E5, E11, FUNCT_1:def 5;
E15:
c
8 . c
12 in rng c
8
by E6, E11, FUNCT_1:def 5;
E16:
c
10 in c
5 . c
12
by E9, E14, SETFAM_1:def 1;
E17:
c
10 in c
8 . c
12
by E10, E15, SETFAM_1:def 1;
( c
5 . c
12 = c
8 . c
12 or c
5 . c
12 misses c
8 . c
12 )
by E12, E13, EQREL_1:def 6;
hence
c
5 . c
11 = c
8 . c
11
by E16, E17, XBOOLE_0:3;
end;
hence
not ( not c
4 = c
7 & not c
4 misses c
7 )
by E5, E6, FUNCT_1:9;
end;
hence
not ( not c
4 = c
7 & not c
4 misses c
7 )
;
end;
end;
end;
c
3 c= bool c
1
then reconsider c
4 = c
3 as
Subset-Family of c
1 ;
c
4 is
a_partition of c
1
by E3, E4, EQREL_1:def 6;
hence
( c
3 is
Element of
bool (bool c1) & c
3 is
a_partition of c
1 & ( for b
1 being
set holds
( b
1 in c
3 iff ex b
2 being
Functionex b
3 being
Subset-Family of c
1 st
(
dom b
2 = c
2 &
rng b
2 = b
3 & ( for b
4 being
set holds
( b
4 in c
2 implies b
2 . b
4 in b
4 ) ) & b
1 = Intersect b
3 & b
1 <> {} ) ) ) )
by E2;
end;
uniqueness
for b1, b2 being a_partition of c1 holds
( ( for b3 being set holds
( b3 in b1 iff ex b4 being Functionex b5 being Subset-Family of c1 st
( dom b4 = c2 & rng b4 = b5 & ( for b6 being set holds
( b6 in c2 implies b4 . b6 in b6 ) ) & b3 = Intersect b5 & b3 <> {} ) ) ) & ( for b3 being set holds
( b3 in b2 iff ex b4 being Functionex b5 being Subset-Family of c1 st
( dom b4 = c2 & rng b4 = b5 & ( for b6 being set holds
( b6 in c2 implies b4 . b6 in b6 ) ) & b3 = Intersect b5 & b3 <> {} ) ) ) implies b1 = b2 )
end;
:: deftheorem Def1 defines '/\' BVFUNC_2:def 1 :
:: deftheorem Def2 defines is_upper_min_depend_of BVFUNC_2:def 2 :
theorem Th2: :: BVFUNC_2:2
proof
let c
1 be non
empty set ;
let c
2 be
Subset of
(PARTITIONS c1);
let c
3 be
Element of c
1;
assume
c
2 <> {}
;
then consider c
4 being
set such that E5:
c
4 in c
2
by XBOOLE_0:def 1;
reconsider c
5 = c
4 as
a_partition of c
1 by E5, PARTIT1:def 3;
E6:
(
union c
5 = c
1 & ( for b
1 being
set holds
( b
1 in c
5 implies ( b
1 <> {} & ( for b
2 being
set holds
not ( b
2 in c
5 & not b
1 = b
2 & not b
1 misses b
2 ) ) ) ) ) )
by EQREL_1:def 6;
E7:
c
1 c= c
1
;
E8:
for b
1 being
a_partition of c
1 holds
( b
1 in c
2 implies c
1 is_a_dependent_set_of b
1 )
by PARTIT1:9;
defpred S
1[
set ] means ( c
3 in a
1 & ( for b
1 being
a_partition of c
1 holds
( b
1 in c
2 implies a
1 is_a_dependent_set_of b
1 ) ) );
reconsider c
6 =
{ b1 where B is Subset of c1 : S1[b1] } as
Subset-Family of c
1 from DOMAIN_1:sch 7();
reconsider c
7 = c
6 as
Subset-Family of c
1 ;
E9:
c
1 in c
7
by E7, E8;
for b
1 being
set holds
( b
1 in c
7 implies c
3 in b
1 )
then E10:
c
3 in meet c
7
by E9, SETFAM_1:def 1;
then E11:
Intersect c
7 <> {}
by E9, SETFAM_1:def 10;
take
Intersect c
7
;
E12:
for b
1 being
a_partition of c
1 holds
( b
1 in c
2 implies
Intersect c
7 is_a_dependent_set_of b
1 )
for b
1 being
set holds
( b
1 c= Intersect c
7 & ( for b
2 being
a_partition of c
1 holds
( b
2 in c
2 implies b
1 is_a_dependent_set_of b
2 ) ) implies b
1 = Intersect c
7 )
proof
let c
8 be
set ;
assume E13:
( c
8 c= Intersect c
7 & ( for b
1 being
a_partition of c
1 holds
( b
1 in c
2 implies c
8 is_a_dependent_set_of b
1 ) ) )
;
then
c
8 is_a_dependent_set_of c
5
by E5;
then consider c
9 being
set such that E14:
( c
9 c= c
5 & c
9 <> {} & c
8 = union c
9 )
by PARTIT1:def 1;
E15:
c
8 c= c
1
by E6, E14, ZFMISC_1:95;
per cases
not ( not c3 in c8 & c3 in c8 )
;
suppose E16:
not c
3 in c
8
;
reconsider c
10 = c
8 as
Subset of c
1 by E6, E14, ZFMISC_1:95;
c
10 ` = c
1 \ c
10
by SUBSET_1:def 5;
then E17:
c
3 in c
10 `
by E16, XBOOLE_0:def 4;
c
10 misses c
10 `
by SUBSET_1:44;
then E18:
c
10 /\ (c10 ` ) = {}
by XBOOLE_0:def 7;
E19:
c
10 <> c
1
by E16;
for b
1 being
a_partition of c
1 holds
( b
1 in c
2 implies c
10 ` is_a_dependent_set_of b
1 )
then E20:
c
10 ` in c
7
by E17;
Intersect c
7 c= c
10 `
then
c
10 /\ (Intersect c7) c= c
10 /\ (c10 ` )
by XBOOLE_1:26;
then E21:
c
10 /\ (Intersect c7) = {}
by E18, XBOOLE_1:3;
c
10 /\ c
10 = c
10
;
then
c
10 c= {}
by E13, E21, XBOOLE_1:26;
then E22:
union c
9 = {}
by E14, XBOOLE_1:3;
consider c
11 being
set such that E23:
c
11 in c
9
by E14, XBOOLE_0:def 1;
E24:
c
11 <> {}
by E6, E14, E23;
E25:
c
11 c= {}
by E22, E23, ZFMISC_1:92;
consider c
12 being
set such that E26:
c
12 in c
11
by E24, XBOOLE_0:def 1;
thus
c
8 = Intersect c
7
by E25, E26;
end;
end;
end;
hence
( c
3 in Intersect c
7 &
Intersect c
7 is_upper_min_depend_of c
2 )
by E9, E10, E12, Def2, SETFAM_1:def 10;
end;
:: deftheorem Def3 defines '\/' BVFUNC_2:def 3 :
theorem Th3: :: BVFUNC_2:3
theorem Th4: :: BVFUNC_2:4
:: deftheorem Def4 defines generating BVFUNC_2:def 4 :
:: deftheorem Def5 defines independent BVFUNC_2:def 5 :
:: deftheorem Def6 defines is_a_coordinate BVFUNC_2:def 6 :
:: deftheorem Def7 defines CompF BVFUNC_2:def 7 :