:: BVFUNC_2 semantic presentation
theorem E1: :: BVFUNC_2:1
definition
let c
1 be non
empty set ;
let c
2 be
Subset of
(PARTITIONS c1);
func '/\' a
2 -> a_partition of a
1 means :
E2:
:: 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 c
2 = {} & not c
2 <> {} )
;
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 E2 defines '/\' BVFUNC_2:def 1 :
:: deftheorem E3 defines is_upper_min_depend_of BVFUNC_2:def 2 :
theorem E4: :: 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 c
3 in c
8 & c
3 in c
8 )
;
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, E3, SETFAM_1:def 10;
end;
:: deftheorem E5 defines '\/' BVFUNC_2:def 3 :
theorem :: BVFUNC_2:3
theorem :: BVFUNC_2:4
:: deftheorem defines generating BVFUNC_2:def 4 :
:: deftheorem defines independent BVFUNC_2:def 5 :
:: deftheorem defines is_a_coordinate BVFUNC_2:def 6 :
:: deftheorem defines CompF BVFUNC_2:def 7 :
:: deftheorem E6 defines is_independent_of BVFUNC_2:def 8 :
:: deftheorem defines All BVFUNC_2:def 9 :
:: deftheorem defines Ex BVFUNC_2:def 10 :
theorem :: BVFUNC_2:5
proof
let c
1 be non
empty set ;
let c
2 be
Subset of
(PARTITIONS c1);
let c
3 be
Element of
Funcs c
1,
BOOLEAN ;
let c
4 be
a_partition of c
1;
let c
5 be
set ;
:: uses BVFUNC_1:def 18
assume E7:
c
5 in CompF c
4,c
2
;
thus
for b
1, b
2 being
set holds
( ( b
1 in c
5 & b
2 in c
5 ) implies (
(All c3,c4,c2) . b
1 = (All c3,c4,c2) . b
2 ) )
proof
let c
6, c
7 be
set ;
assume E8:
( c
6 in c
5 & c
7 in c
5 )
;
then reconsider c
8 = c
6, c
9 = c
7 as
Element of c
1 by E7;
E9:
( c
9 in EqClass c
9,
(CompF c4,c2) &
EqClass c
9,
(CompF c4,c2) in CompF c
4,c
2 )
by T_1TOPSP:def 1;
( c
5 = EqClass c
9,
(CompF c4,c2) or c
5 misses EqClass c
9,
(CompF c4,c2) )
by E7, EQREL_1:def 6;
then E10:
EqClass c
8,
(CompF c4,c2) = EqClass c
9,
(CompF c4,c2)
by E8, E9, T_1TOPSP:def 1, XBOOLE_0:3;
per cases
not ( not ( for b
1 being
Element of c
1 holds
( b
1 in EqClass c
8,
(CompF c4,c2) implies c
3 . b
1 = TRUE ) & for b
1 being
Element of c
1 holds
( b
1 in EqClass c
9,
(CompF c4,c2) implies c
3 . b
1 = TRUE ) ) & not ( for b
1 being
Element of c
1 holds
( b
1 in EqClass c
8,
(CompF c4,c2) implies c
3 . b
1 = TRUE ) & ex b
1 being
Element of c
1 st
( b
1 in EqClass c
9,
(CompF c4,c2) & not c
3 . b
1 = TRUE ) ) & not ( ex b
1 being
Element of c
1 st
( b
1 in EqClass c
8,
(CompF c4,c2) & not c
3 . b
1 = TRUE ) & for b
1 being
Element of c
1 holds
( b
1 in EqClass c
9,
(CompF c4,c2) implies c
3 . b
1 = TRUE ) ) & not ( ex b
1 being
Element of c
1 st
( b
1 in EqClass c
8,
(CompF c4,c2) & not c
3 . b
1 = TRUE ) & ex b
1 being
Element of c
1 st
( b
1 in EqClass c
9,
(CompF c4,c2) & not c
3 . b
1 = TRUE ) ) )
;