let T be TopSpace; :: thesis: LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #) is C_Lattice
set L = LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #);
LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #) is Lattice-like
proof
thus for a, b being Element of LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #) holds a "\/" b = b "\/" a :: according to LATTICES:def 4,LATTICES:def 10 :: thesis: ( LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #) is join-associative & LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #) is meet-absorbing & LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #) is meet-commutative & LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #) is meet-associative & LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #) is join-absorbing )
proof
let a, b be Element of LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #); :: thesis: a "\/" b = b "\/" a
reconsider A = a, B = b as Element of Domains_of T ;
thus a "\/" b = (Int (Cl (B \/ A))) \/ (B \/ A) by Def2
.= b "\/" a by Def2 ; :: thesis: verum
end;
thus for a, b, c being Element of LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #) holds a "\/" (b "\/" c) = (a "\/" b) "\/" c :: according to LATTICES:def 5 :: thesis: ( LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #) is meet-absorbing & LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #) is meet-commutative & LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #) is meet-associative & LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #) is join-absorbing )
proof
let a, b, c be Element of LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #); :: thesis: a "\/" (b "\/" c) = (a "\/" b) "\/" c
reconsider A = a, B = b, C = c as Element of Domains_of T ;
A1: b "\/" c = (Int (Cl (B \/ C))) \/ (B \/ C) by Def2;
A2: a "\/" b = (Int (Cl (A \/ B))) \/ (A \/ B) by Def2;
thus a "\/" (b "\/" c) = (Int (Cl (A \/ ((Int (Cl (B \/ C))) \/ (B \/ C))))) \/ (A \/ ((Int (Cl (B \/ C))) \/ (B \/ C))) by A1, Def2
.= (Int (Cl (A \/ (B \/ C)))) \/ (A \/ (B \/ C)) by Th10
.= (Int (Cl (A \/ (B \/ C)))) \/ ((A \/ B) \/ C) by XBOOLE_1:4
.= (Int (Cl ((A \/ B) \/ C))) \/ ((A \/ B) \/ C) by XBOOLE_1:4
.= (Int (Cl (((Int (Cl (A \/ B))) \/ (A \/ B)) \/ C))) \/ (((Int (Cl (A \/ B))) \/ (A \/ B)) \/ C) by Th10
.= (a "\/" b) "\/" c by A2, Def2 ; :: thesis: verum
end;
thus for a, b being Element of LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #) holds (a "/\" b) "\/" b = b :: according to LATTICES:def 8 :: thesis: ( LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #) is meet-commutative & LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #) is meet-associative & LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #) is join-absorbing )
proof
let a, b be Element of LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #); :: thesis: (a "/\" b) "\/" b = b
reconsider A = a, B = b as Element of Domains_of T ;
A3: a "/\" b = (Cl (Int (A /\ B))) /\ (A /\ B) by Def3;
A4: ( (Cl (Int (A /\ B))) /\ (A /\ B) c= A /\ B & A /\ B c= B ) by XBOOLE_1:17;
B in { D where D is Subset of T : D is condensed } ;
then ex D being Subset of T st
( D = B & D is condensed ) ;
then A5: Int (Cl B) c= B by TOPS_1:def 6;
thus (a "/\" b) "\/" b = (Int (Cl (((Cl (Int (A /\ B))) /\ (A /\ B)) \/ B))) \/ (((Cl (Int (A /\ B))) /\ (A /\ B)) \/ B) by A3, Def2
.= (Int (Cl (((Cl (Int (A /\ B))) /\ (A /\ B)) \/ B))) \/ B by A4, XBOOLE_1:1, XBOOLE_1:12
.= (Int (Cl B)) \/ B by A4, XBOOLE_1:1, XBOOLE_1:12
.= b by A5, XBOOLE_1:12 ; :: thesis: verum
end;
thus for a, b being Element of LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #) holds a "/\" b = b "/\" a :: according to LATTICES:def 6 :: thesis: ( LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #) is meet-associative & LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #) is join-absorbing )
proof
let a, b be Element of LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #); :: thesis: a "/\" b = b "/\" a
reconsider A = a, B = b as Element of Domains_of T ;
thus a "/\" b = (Cl (Int (B /\ A))) /\ (B /\ A) by Def3
.= b "/\" a by Def3 ; :: thesis: verum
end;
thus for a, b, c being Element of LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #) holds a "/\" (b "/\" c) = (a "/\" b) "/\" c :: according to LATTICES:def 7 :: thesis: LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #) is join-absorbing
proof
let a, b, c be Element of LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #); :: thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c
reconsider A = a, B = b, C = c as Element of Domains_of T ;
A6: b "/\" c = (Cl (Int (B /\ C))) /\ (B /\ C) by Def3;
A7: a "/\" b = (Cl (Int (A /\ B))) /\ (A /\ B) by Def3;
thus a "/\" (b "/\" c) = (Cl (Int (A /\ ((Cl (Int (B /\ C))) /\ (B /\ C))))) /\ (A /\ ((Cl (Int (B /\ C))) /\ (B /\ C))) by A6, Def3
.= (Cl (Int (A /\ (B /\ C)))) /\ (A /\ (B /\ C)) by Th12
.= (Cl (Int (A /\ (B /\ C)))) /\ ((A /\ B) /\ C) by XBOOLE_1:16
.= (Cl (Int ((A /\ B) /\ C))) /\ ((A /\ B) /\ C) by XBOOLE_1:16
.= (Cl (Int (((Cl (Int (A /\ B))) /\ (A /\ B)) /\ C))) /\ (((Cl (Int (A /\ B))) /\ (A /\ B)) /\ C) by Th12
.= (a "/\" b) "/\" c by A7, Def3 ; :: thesis: verum
end;
thus for a, b being Element of LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #) holds a "/\" (a "\/" b) = a :: according to LATTICES:def 9 :: thesis: verum
proof
let a, b be Element of LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #); :: thesis: a "/\" (a "\/" b) = a
reconsider A = a, B = b as Element of Domains_of T ;
A8: a "\/" b = (Int (Cl (A \/ B))) \/ (A \/ B) by Def2;
A9: ( A c= A \/ B & A \/ B c= (Int (Cl (A \/ B))) \/ (A \/ B) ) by XBOOLE_1:7;
A in { D where D is Subset of T : D is condensed } ;
then ex D being Subset of T st
( D = A & D is condensed ) ;
then A10: A c= Cl (Int A) by TOPS_1:def 6;
thus a "/\" (a "\/" b) = (Cl (Int (A /\ ((Int (Cl (A \/ B))) \/ (A \/ B))))) /\ (A /\ ((Int (Cl (A \/ B))) \/ (A \/ B))) by A8, Def3
.= (Cl (Int (A /\ ((Int (Cl (A \/ B))) \/ (A \/ B))))) /\ A by A9, XBOOLE_1:1, XBOOLE_1:28
.= (Cl (Int A)) /\ A by A9, XBOOLE_1:1, XBOOLE_1:28
.= a by A10, XBOOLE_1:28 ; :: thesis: verum
end;
end;
then reconsider L = LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #) as Lattice ;
L is bounded
proof
thus L is lower-bounded :: according to LATTICES:def 15 :: thesis: L is upper-bounded
proof
{} T is condensed by Th14;
then {} T in { D where D is Subset of T : D is condensed } ;
then reconsider c = {} T as Element of L ;
take c ; :: according to LATTICES:def 13 :: thesis: for b1 being Element of the carrier of L holds
( c "/\" b1 = c & b1 "/\" c = c )
let a be Element of L; :: thesis: ( c "/\" a = c & a "/\" c = c )
reconsider C = c, A = a as Element of Domains_of T ;
C /\ A = C ;
hence c "/\" a = (Cl (Int C)) /\ C by Def3
.= c ;
:: thesis: a "/\" c = c
hence a "/\" c = c ; :: thesis: verum
end;
thus L is upper-bounded :: thesis: verum
proof
[#] T is condensed by Th15;
then [#] T in { D where D is Subset of T : D is condensed } ;
then reconsider c = [#] T as Element of L ;
take c ; :: according to LATTICES:def 14 :: thesis: for b1 being Element of the carrier of L holds
( c "\/" b1 = c & b1 "\/" c = c )
let a be Element of L; :: thesis: ( c "\/" a = c & a "\/" c = c )
reconsider C = c, A = a as Element of Domains_of T ;
C \/ A = C by XBOOLE_1:12;
hence c "\/" a = (Int (Cl C)) \/ C by Def2
.= c by XBOOLE_1:12 ;
:: thesis: a "\/" c = c
hence a "\/" c = c ; :: thesis: verum
end;
end;
then reconsider L = L as 01_Lattice ;
L is complemented
proof
let b be Element of L; :: according to LATTICES:def 19 :: thesis: ex b1 being Element of the carrier of L st b1 is_a_complement_of b
reconsider B = b as Element of Domains_of T ;
B in { D where D is Subset of T : D is condensed } ;
then ex D being Subset of T st
( D = B & D is condensed ) ;
then B ` is condensed by Th16;
then B ` in { D where D is Subset of T : D is condensed } ;
then reconsider a = B ` as Element of L ;
take a ; :: thesis: a is_a_complement_of b
[#] T is condensed by Th15;
then [#] T in { D where D is Subset of T : D is condensed } ;
then reconsider c = [#] T as Element of L ;
A11: for v being Element of L holds the L_meet of L . c,v = v
proof
let v be Element of L; :: thesis: the L_meet of L . c,v = v
reconsider V = v as Element of Domains_of T ;
V in { D where D is Subset of T : D is condensed } ;
then ex D being Subset of T st
( D = V & D is condensed ) ;
then A12: V c= Cl (Int V) by TOPS_1:def 6;
thus the L_meet of L . c,v = (Cl (Int (([#] T) /\ V))) /\ (([#] T) /\ V) by Def3
.= (Cl (Int (([#] T) /\ V))) /\ V by XBOOLE_1:28
.= (Cl (Int V)) /\ V by XBOOLE_1:28
.= v by A12, XBOOLE_1:28 ; :: thesis: verum
end;
thus a "\/" b = (Int (Cl ((B ` ) \/ B))) \/ ((B ` ) \/ B) by Def2
.= (Int (Cl ((B ` ) \/ B))) \/ ([#] T) by PRE_TOPC:18
.= c by XBOOLE_1:12
.= Top L by A11, LATTICE2:25 ; :: according to LATTICES:def 18 :: thesis: ( b "\/" a = Top L & a "/\" b = Bottom L & b "/\" a = Bottom L )
hence b "\/" a = Top L ; :: thesis: ( a "/\" b = Bottom L & b "/\" a = Bottom L )
{} T is condensed by Th14;
then {} T in { D where D is Subset of T : D is condensed } ;
then reconsider c = {} T as Element of L ;
A13: for v being Element of L holds the L_join of L . c,v = v
proof
let v be Element of L; :: thesis: the L_join of L . c,v = v
reconsider V = v as Element of Domains_of T ;
V in { D where D is Subset of T : D is condensed } ;
then ex D being Subset of T st
( D = V & D is condensed ) ;
then A14: Int (Cl V) c= V by TOPS_1:def 6;
thus the L_join of L . c,v = (Int (Cl (({} T) \/ V))) \/ (({} T) \/ V) by Def2
.= (Int (Cl ((([#] T) ` ) \/ V))) \/ (({} T) \/ V) by XBOOLE_1:37
.= (Int (Cl ((([#] T) ` ) \/ ((V ` ) ` )))) \/ ((([#] T) ` ) \/ V) by XBOOLE_1:37
.= (Int (Cl ((([#] T) /\ (V ` )) ` ))) \/ ((([#] T) ` ) \/ ((V ` ) ` )) by XBOOLE_1:54
.= (Int (Cl ((([#] T) /\ (V ` )) ` ))) \/ ((([#] T) /\ (V ` )) ` ) by XBOOLE_1:54
.= (Int (Cl ((V ` ) ` ))) \/ ((([#] T) /\ (V ` )) ` ) by XBOOLE_1:28
.= (Int (Cl V)) \/ ((V ` ) ` ) by XBOOLE_1:28
.= v by A14, XBOOLE_1:12 ; :: thesis: verum
end;
A15: B ` misses B by XBOOLE_1:79;
thus a "/\" b = (Cl (Int ((B ` ) /\ B))) /\ ((B ` ) /\ B) by Def3
.= (Cl (Int ((B ` ) /\ B))) /\ ({} T) by A15, XBOOLE_0:def 7
.= Bottom L by A13, LATTICE2:22 ; :: thesis: b "/\" a = Bottom L
hence b "/\" a = Bottom L ; :: thesis: verum
end;
hence LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #) is C_Lattice ; :: thesis: verum