:: TDLAT_1 semantic presentation
begin
theorem Th1: :: TDLAT_1:1
for T being 1-sorted
for A, B being Subset of T holds
( A \/ B = [#] T iff A ` c= B )
proof
let T be 1-sorted ; ::_thesis: for A, B being Subset of T holds
( A \/ B = [#] T iff A ` c= B )
let A, B be Subset of T; ::_thesis: ( A \/ B = [#] T iff A ` c= B )
hereby ::_thesis: ( A ` c= B implies A \/ B = [#] T )
assume A \/ B = [#] T ; ::_thesis: A ` c= B
then ([#] T) \ A = B \ A by XBOOLE_1:40;
hence A ` c= B by XBOOLE_1:36; ::_thesis: verum
end;
assume A ` c= B ; ::_thesis: A \/ B = [#] T
then A \/ (A `) c= A \/ B by XBOOLE_1:9;
then [#] T c= A \/ B by PRE_TOPC:2;
hence A \/ B = [#] T by XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th2: :: TDLAT_1:2
for T being 1-sorted
for A, B being Subset of T holds
( A misses B iff B c= A ` ) by SUBSET_1:23;
theorem Th3: :: TDLAT_1:3
for T being TopSpace
for A being Subset of T holds Cl (Int (Cl A)) c= Cl A
proof
let T be TopSpace; ::_thesis: for A being Subset of T holds Cl (Int (Cl A)) c= Cl A
let A be Subset of T; ::_thesis: Cl (Int (Cl A)) c= Cl A
Cl (Int (Cl A)) c= Cl (Cl A) by PRE_TOPC:19, TOPS_1:16;
hence Cl (Int (Cl A)) c= Cl A ; ::_thesis: verum
end;
theorem Th4: :: TDLAT_1:4
for T being TopSpace
for A being Subset of T holds Int A c= Int (Cl (Int A))
proof
let T be TopSpace; ::_thesis: for A being Subset of T holds Int A c= Int (Cl (Int A))
let A be Subset of T; ::_thesis: Int A c= Int (Cl (Int A))
Int (Int A) c= Int (Cl (Int A)) by PRE_TOPC:18, TOPS_1:19;
hence Int A c= Int (Cl (Int A)) ; ::_thesis: verum
end;
theorem Th5: :: TDLAT_1:5
for T being TopSpace
for A being Subset of T holds Int (Cl A) = Int (Cl (Int (Cl A)))
proof
let T be TopSpace; ::_thesis: for A being Subset of T holds Int (Cl A) = Int (Cl (Int (Cl A)))
let A be Subset of T; ::_thesis: Int (Cl A) = Int (Cl (Int (Cl A)))
A1: Int (Int (Cl A)) c= Int (Cl (Int (Cl A))) by PRE_TOPC:18, TOPS_1:19;
Int (Cl (Int (Cl A))) c= Int (Cl A) by Th3, TOPS_1:19;
hence Int (Cl A) = Int (Cl (Int (Cl A))) by A1, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th6: :: TDLAT_1:6
for T being TopSpace
for A, B being Subset of T st ( A is closed or B is closed ) holds
(Cl (Int A)) \/ (Cl (Int B)) = Cl (Int (A \/ B))
proof
let T be TopSpace; ::_thesis: for A, B being Subset of T st ( A is closed or B is closed ) holds
(Cl (Int A)) \/ (Cl (Int B)) = Cl (Int (A \/ B))
let A, B be Subset of T; ::_thesis: ( ( A is closed or B is closed ) implies (Cl (Int A)) \/ (Cl (Int B)) = Cl (Int (A \/ B)) )
A1: (A \/ B) \/ ((A \/ B) `) c= (A \/ B) \/ (Cl ((A \/ B) `)) by PRE_TOPC:18, XBOOLE_1:9;
(A \/ B) \/ ((A \/ B) `) = [#] T by PRE_TOPC:2;
then A2: (A \/ B) \/ (Cl ((A \/ B) `)) = [#] T by A1, XBOOLE_0:def_10;
then A \/ (B \/ (Cl ((A \/ B) `))) = [#] T by XBOOLE_1:4;
then A ` c= B \/ (Cl ((A \/ B) `)) by Th1;
then A3: Cl (A `) c= Cl (B \/ (Cl ((A \/ B) `))) by PRE_TOPC:19;
B \/ (A \/ (Cl ((A \/ B) `))) = [#] T by A2, XBOOLE_1:4;
then B ` c= A \/ (Cl ((A \/ B) `)) by Th1;
then A4: Cl (B `) c= Cl (A \/ (Cl ((A \/ B) `))) by PRE_TOPC:19;
assume A5: ( A is closed or B is closed ) ; ::_thesis: (Cl (Int A)) \/ (Cl (Int B)) = Cl (Int (A \/ B))
A6: now__::_thesis:_Cl_(Int_(A_\/_B))_c=_(Cl_(Int_A))_\/_(Cl_(Int_B))
percases ( A is closed or B is closed ) by A5;
suppose A is closed ; ::_thesis: Cl (Int (A \/ B)) c= (Cl (Int A)) \/ (Cl (Int B))
then ((Cl (B `)) `) ` c= A \/ (Cl ((B \/ A) `)) by A4, PRE_TOPC:22;
then ((Cl (B `)) `) \/ (A \/ (Cl ((B \/ A) `))) = [#] T by Th1;
then (Int B) \/ (A \/ (Cl ((B \/ A) `))) = [#] T by TOPS_1:def_1;
then A \/ ((Int B) \/ (Cl ((B \/ A) `))) = [#] T by XBOOLE_1:4;
then A ` c= (Int B) \/ (Cl ((B \/ A) `)) by Th1;
then Cl (A `) c= Cl ((Int B) \/ (Cl ((B \/ A) `))) by PRE_TOPC:19;
then Cl (A `) c= (Cl (Int B)) \/ (Cl (Cl ((B \/ A) `))) by PRE_TOPC:20;
then (Cl (A `)) \/ ((Cl (A `)) `) c= ((Cl (Int B)) \/ (Cl ((B \/ A) `))) \/ ((Cl (A `)) `) by XBOOLE_1:9;
then [#] T c= ((Cl (Int B)) \/ (Cl ((B \/ A) `))) \/ ((Cl (A `)) `) by PRE_TOPC:2;
then [#] T c= ((Cl ((B \/ A) `)) \/ (Cl (Int B))) \/ (Int A) by TOPS_1:def_1;
then [#] T c= (Cl ((B \/ A) `)) \/ ((Cl (Int B)) \/ (Int A)) by XBOOLE_1:4;
then [#] T = (Cl ((B \/ A) `)) \/ ((Cl (Int B)) \/ (Int A)) by XBOOLE_0:def_10;
then (Cl ((B \/ A) `)) ` c= (Cl (Int B)) \/ (Int A) by Th1;
then Int (B \/ A) c= (Cl (Int B)) \/ (Int A) by TOPS_1:def_1;
then Cl (Int (B \/ A)) c= Cl ((Cl (Int B)) \/ (Int A)) by PRE_TOPC:19;
then Cl (Int (B \/ A)) c= (Cl (Cl (Int B))) \/ (Cl (Int A)) by PRE_TOPC:20;
hence Cl (Int (A \/ B)) c= (Cl (Int A)) \/ (Cl (Int B)) ; ::_thesis: verum
end;
suppose B is closed ; ::_thesis: Cl (Int (A \/ B)) c= (Cl (Int A)) \/ (Cl (Int B))
then ((Cl (A `)) `) ` c= B \/ (Cl ((A \/ B) `)) by A3, PRE_TOPC:22;
then ((Cl (A `)) `) \/ (B \/ (Cl ((A \/ B) `))) = [#] T by Th1;
then (Int A) \/ (B \/ (Cl ((A \/ B) `))) = [#] T by TOPS_1:def_1;
then B \/ ((Int A) \/ (Cl ((A \/ B) `))) = [#] T by XBOOLE_1:4;
then B ` c= (Int A) \/ (Cl ((A \/ B) `)) by Th1;
then Cl (B `) c= Cl ((Int A) \/ (Cl ((A \/ B) `))) by PRE_TOPC:19;
then Cl (B `) c= (Cl (Int A)) \/ (Cl (Cl ((A \/ B) `))) by PRE_TOPC:20;
then (Cl (B `)) \/ ((Cl (B `)) `) c= ((Cl (Int A)) \/ (Cl ((A \/ B) `))) \/ ((Cl (B `)) `) by XBOOLE_1:9;
then [#] T c= ((Cl (Int A)) \/ (Cl ((A \/ B) `))) \/ ((Cl (B `)) `) by PRE_TOPC:2;
then [#] T c= ((Cl ((A \/ B) `)) \/ (Cl (Int A))) \/ (Int B) by TOPS_1:def_1;
then [#] T c= (Cl ((A \/ B) `)) \/ ((Cl (Int A)) \/ (Int B)) by XBOOLE_1:4;
then [#] T = (Cl ((A \/ B) `)) \/ ((Cl (Int A)) \/ (Int B)) by XBOOLE_0:def_10;
then (Cl ((A \/ B) `)) ` c= (Cl (Int A)) \/ (Int B) by Th1;
then Int (A \/ B) c= (Cl (Int A)) \/ (Int B) by TOPS_1:def_1;
then Cl (Int (A \/ B)) c= Cl ((Cl (Int A)) \/ (Int B)) by PRE_TOPC:19;
then Cl (Int (A \/ B)) c= (Cl (Cl (Int A))) \/ (Cl (Int B)) by PRE_TOPC:20;
hence Cl (Int (A \/ B)) c= (Cl (Int A)) \/ (Cl (Int B)) ; ::_thesis: verum
end;
end;
end;
Int B c= Int (A \/ B) by TOPS_1:19, XBOOLE_1:7;
then A7: Cl (Int B) c= Cl (Int (A \/ B)) by PRE_TOPC:19;
Int A c= Int (A \/ B) by TOPS_1:19, XBOOLE_1:7;
then Cl (Int A) c= Cl (Int (A \/ B)) by PRE_TOPC:19;
then (Cl (Int A)) \/ (Cl (Int B)) c= Cl (Int (A \/ B)) by A7, XBOOLE_1:8;
hence (Cl (Int A)) \/ (Cl (Int B)) = Cl (Int (A \/ B)) by A6, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th7: :: TDLAT_1:7
for T being TopSpace
for A, B being Subset of T st ( A is open or B is open ) holds
(Int (Cl A)) /\ (Int (Cl B)) = Int (Cl (A /\ B))
proof
let T be TopSpace; ::_thesis: for A, B being Subset of T st ( A is open or B is open ) holds
(Int (Cl A)) /\ (Int (Cl B)) = Int (Cl (A /\ B))
let A, B be Subset of T; ::_thesis: ( ( A is open or B is open ) implies (Int (Cl A)) /\ (Int (Cl B)) = Int (Cl (A /\ B)) )
A1: Int (A `) misses (Int (A `)) ` by XBOOLE_1:79;
A2: Int (B `) misses (Int (B `)) ` by XBOOLE_1:79;
A /\ B misses (A /\ B) ` by XBOOLE_1:79;
then A3: {} T = (A /\ B) /\ ((A /\ B) `) by XBOOLE_0:def_7;
A4: (A /\ B) /\ (Int ((A /\ B) `)) c= (A /\ B) /\ ((A /\ B) `) by TOPS_1:16, XBOOLE_1:26;
then A /\ (B /\ (Int ((A /\ B) `))) = {} T by A3, XBOOLE_1:16;
then A misses B /\ (Int ((A /\ B) `)) by XBOOLE_0:def_7;
then B /\ (Int ((A /\ B) `)) c= A ` by Th2;
then A5: Int (B /\ (Int ((A /\ B) `))) c= Int (A `) by TOPS_1:19;
B /\ (A /\ (Int ((A /\ B) `))) = {} T by A3, A4, XBOOLE_1:16;
then B misses A /\ (Int ((A /\ B) `)) by XBOOLE_0:def_7;
then A /\ (Int ((A /\ B) `)) c= B ` by Th2;
then A6: Int (A /\ (Int ((A /\ B) `))) c= Int (B `) by TOPS_1:19;
assume A7: ( A is open or B is open ) ; ::_thesis: (Int (Cl A)) /\ (Int (Cl B)) = Int (Cl (A /\ B))
A8: now__::_thesis:_(Int_(Cl_A))_/\_(Int_(Cl_B))_c=_Int_(Cl_(A_/\_B))
percases ( A is open or B is open ) by A7;
suppose A is open ; ::_thesis: (Int (Cl A)) /\ (Int (Cl B)) c= Int (Cl (A /\ B))
then A /\ (Int ((A /\ B) `)) c= ((Int (B `)) `) ` by A6, TOPS_1:23;
then (Int (B `)) ` misses A /\ (Int ((A /\ B) `)) by Th2;
then ((Int (B `)) `) /\ (A /\ (Int ((A /\ B) `))) = {} by XBOOLE_0:def_7;
then (((Cl ((B `) `)) `) `) /\ (A /\ (Int ((A /\ B) `))) = {} by TOPS_1:def_1;
then A /\ ((Cl B) /\ (Int ((A /\ B) `))) = {} by XBOOLE_1:16;
then A misses (Cl B) /\ (Int ((A /\ B) `)) by XBOOLE_0:def_7;
then (Cl B) /\ (Int ((A /\ B) `)) c= A ` by Th2;
then Int ((Cl B) /\ (Int ((A /\ B) `))) c= Int (A `) by TOPS_1:19;
then (Int (Cl B)) /\ (Int (Int ((A /\ B) `))) c= Int (A `) by TOPS_1:17;
then ((Int (Cl B)) /\ (Int ((A /\ B) `))) /\ ((Int (A `)) `) c= (Int (A `)) /\ ((Int (A `)) `) by XBOOLE_1:26;
then ((Int (Cl B)) /\ (Int ((A /\ B) `))) /\ ((Int (A `)) `) c= {} T by A1, XBOOLE_0:def_7;
then ((Int (Cl B)) /\ (Int ((A /\ B) `))) /\ (((Cl ((A `) `)) `) `) c= {} T by TOPS_1:def_1;
then {} T = (Int ((A /\ B) `)) /\ ((Int (Cl B)) /\ (Cl A)) by XBOOLE_1:16;
then Int ((A /\ B) `) misses (Int (Cl B)) /\ (Cl A) by XBOOLE_0:def_7;
then (Int (Cl B)) /\ (Cl A) c= (Int ((A /\ B) `)) ` by Th2;
then (Int (Cl B)) /\ (Cl A) c= ((Cl (((A /\ B) `) `)) `) ` by TOPS_1:def_1;
then Int ((Int (Cl B)) /\ (Cl A)) c= Int (Cl (B /\ A)) by TOPS_1:19;
then (Int (Int (Cl B))) /\ (Int (Cl A)) c= Int (Cl (B /\ A)) by TOPS_1:17;
hence (Int (Cl A)) /\ (Int (Cl B)) c= Int (Cl (A /\ B)) ; ::_thesis: verum
end;
suppose B is open ; ::_thesis: (Int (Cl A)) /\ (Int (Cl B)) c= Int (Cl (A /\ B))
then B /\ (Int ((A /\ B) `)) c= ((Int (A `)) `) ` by A5, TOPS_1:23;
then (Int (A `)) ` misses B /\ (Int ((A /\ B) `)) by Th2;
then ((Int (A `)) `) /\ (B /\ (Int ((A /\ B) `))) = {} T by XBOOLE_0:def_7;
then (((Cl ((A `) `)) `) `) /\ (B /\ (Int ((A /\ B) `))) = {} T by TOPS_1:def_1;
then B /\ ((Cl A) /\ (Int ((A /\ B) `))) = {} T by XBOOLE_1:16;
then B misses (Cl A) /\ (Int ((A /\ B) `)) by XBOOLE_0:def_7;
then (Cl A) /\ (Int ((A /\ B) `)) c= B ` by Th2;
then Int ((Cl A) /\ (Int ((A /\ B) `))) c= Int (B `) by TOPS_1:19;
then (Int (Cl A)) /\ (Int (Int ((A /\ B) `))) c= Int (B `) by TOPS_1:17;
then ((Int (Cl A)) /\ (Int ((A /\ B) `))) /\ ((Int (B `)) `) c= (Int (B `)) /\ ((Int (B `)) `) by XBOOLE_1:26;
then ((Int (Cl A)) /\ (Int ((A /\ B) `))) /\ ((Int (B `)) `) c= {} T by A2, XBOOLE_0:def_7;
then ((Int (Cl A)) /\ (Int ((A /\ B) `))) /\ (((Cl ((B `) `)) `) `) c= {} T by TOPS_1:def_1;
then {} T = (Int ((A /\ B) `)) /\ ((Int (Cl A)) /\ (Cl B)) by XBOOLE_1:16;
then Int ((A /\ B) `) misses (Int (Cl A)) /\ (Cl B) by XBOOLE_0:def_7;
then (Int (Cl A)) /\ (Cl B) c= (Int ((A /\ B) `)) ` by Th2;
then (Int (Cl A)) /\ (Cl B) c= ((Cl (((A /\ B) `) `)) `) ` by TOPS_1:def_1;
then Int ((Int (Cl A)) /\ (Cl B)) c= Int (Cl (A /\ B)) by TOPS_1:19;
then (Int (Int (Cl A))) /\ (Int (Cl B)) c= Int (Cl (A /\ B)) by TOPS_1:17;
hence (Int (Cl A)) /\ (Int (Cl B)) c= Int (Cl (A /\ B)) ; ::_thesis: verum
end;
end;
end;
Cl (A /\ B) c= Cl B by PRE_TOPC:19, XBOOLE_1:17;
then A9: Int (Cl (A /\ B)) c= Int (Cl B) by TOPS_1:19;
Cl (A /\ B) c= Cl A by PRE_TOPC:19, XBOOLE_1:17;
then Int (Cl (A /\ B)) c= Int (Cl A) by TOPS_1:19;
then Int (Cl (A /\ B)) c= (Int (Cl A)) /\ (Int (Cl B)) by A9, XBOOLE_1:19;
hence (Int (Cl A)) /\ (Int (Cl B)) = Int (Cl (A /\ B)) by A8, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th8: :: TDLAT_1:8
for T being TopSpace
for A being Subset of T holds Int (A /\ (Cl (A `))) = {} T
proof
let T be TopSpace; ::_thesis: for A being Subset of T holds Int (A /\ (Cl (A `))) = {} T
let A be Subset of T; ::_thesis: Int (A /\ (Cl (A `))) = {} T
A1: Int A misses (Int A) ` by XBOOLE_1:79;
thus Int (A /\ (Cl (A `))) = Int (A /\ (((Cl (A `)) `) `))
.= Int (A /\ ((Int A) `)) by TOPS_1:def_1
.= (Int (Int A)) /\ (Int ((Int A) `)) by TOPS_1:17
.= Int ((Int A) /\ ((Int A) `)) by TOPS_1:17
.= Int ({} T) by A1, XBOOLE_0:def_7
.= {} T ; ::_thesis: verum
end;
theorem Th9: :: TDLAT_1:9
for T being TopSpace
for A being Subset of T holds Cl (A \/ (Int (A `))) = [#] T
proof
let T be TopSpace; ::_thesis: for A being Subset of T holds Cl (A \/ (Int (A `))) = [#] T
let A be Subset of T; ::_thesis: Cl (A \/ (Int (A `))) = [#] T
thus Cl (A \/ (Int (A `))) = Cl (A \/ ((Cl ((A `) `)) `)) by TOPS_1:def_1
.= (Cl (Cl A)) \/ (Cl ((Cl A) `)) by PRE_TOPC:20
.= Cl ((Cl A) \/ ((Cl A) `)) by PRE_TOPC:20
.= Cl ([#] T) by PRE_TOPC:2
.= [#] T by TOPS_1:2 ; ::_thesis: verum
end;
theorem Th10: :: TDLAT_1:10
for T being TopSpace
for A, B being Subset of T holds (Int (Cl (A \/ ((Int (Cl B)) \/ B)))) \/ (A \/ ((Int (Cl B)) \/ B)) = (Int (Cl (A \/ B))) \/ (A \/ B)
proof
let T be TopSpace; ::_thesis: for A, B being Subset of T holds (Int (Cl (A \/ ((Int (Cl B)) \/ B)))) \/ (A \/ ((Int (Cl B)) \/ B)) = (Int (Cl (A \/ B))) \/ (A \/ B)
let A, B be Subset of T; ::_thesis: (Int (Cl (A \/ ((Int (Cl B)) \/ B)))) \/ (A \/ ((Int (Cl B)) \/ B)) = (Int (Cl (A \/ B))) \/ (A \/ B)
Cl B c= Cl (A \/ B) by PRE_TOPC:19, XBOOLE_1:7;
then A1: Int (Cl B) c= Int (Cl (A \/ B)) by TOPS_1:19;
A \/ B c= A \/ ((Int (Cl B)) \/ B) by XBOOLE_1:7, XBOOLE_1:9;
then Cl (A \/ B) c= Cl (A \/ ((Int (Cl B)) \/ B)) by PRE_TOPC:19;
then A2: Int (Cl (A \/ B)) c= Int (Cl (A \/ ((Int (Cl B)) \/ B))) by TOPS_1:19;
Int (Cl (A \/ ((Int (Cl B)) \/ B))) c= (Int (Cl (A \/ ((Int (Cl B)) \/ B)))) \/ (Int (Cl B)) by XBOOLE_1:7;
then A3: Int (Cl (A \/ B)) c= (Int (Cl (A \/ ((Int (Cl B)) \/ B)))) \/ (Int (Cl B)) by A2, XBOOLE_1:1;
Int (Cl (A \/ ((Int (Cl B)) \/ B))) = Int (Cl ((A \/ (Int (Cl B))) \/ B)) by XBOOLE_1:4
.= Int ((Cl (A \/ (Int (Cl B)))) \/ (Cl B)) by PRE_TOPC:20
.= Int (((Cl A) \/ (Cl (Int (Cl B)))) \/ (Cl B)) by PRE_TOPC:20
.= Int ((Cl A) \/ ((Cl (Int (Cl B))) \/ (Cl B))) by XBOOLE_1:4
.= Int ((Cl A) \/ (Cl B)) by Th3, XBOOLE_1:12
.= Int (Cl (A \/ B)) by PRE_TOPC:20 ;
then (Int (Cl (A \/ ((Int (Cl B)) \/ B)))) \/ (Int (Cl B)) c= Int (Cl (A \/ B)) by A1, XBOOLE_1:8;
then A4: (Int (Cl (A \/ ((Int (Cl B)) \/ B)))) \/ (Int (Cl B)) = Int (Cl (A \/ B)) by A3, XBOOLE_0:def_10;
A \/ ((Int (Cl B)) \/ B) = (Int (Cl B)) \/ (A \/ B) by XBOOLE_1:4;
hence (Int (Cl (A \/ ((Int (Cl B)) \/ B)))) \/ (A \/ ((Int (Cl B)) \/ B)) = (Int (Cl (A \/ B))) \/ (A \/ B) by A4, XBOOLE_1:4; ::_thesis: verum
end;
theorem :: TDLAT_1:11
for T being TopSpace
for A, C being Subset of T holds (Int (Cl (((Int (Cl A)) \/ A) \/ C))) \/ (((Int (Cl A)) \/ A) \/ C) = (Int (Cl (A \/ C))) \/ (A \/ C) by Th10;
theorem Th12: :: TDLAT_1:12
for T being TopSpace
for A, B being Subset of T holds (Cl (Int (A /\ ((Cl (Int B)) /\ B)))) /\ (A /\ ((Cl (Int B)) /\ B)) = (Cl (Int (A /\ B))) /\ (A /\ B)
proof
let T be TopSpace; ::_thesis: for A, B being Subset of T holds (Cl (Int (A /\ ((Cl (Int B)) /\ B)))) /\ (A /\ ((Cl (Int B)) /\ B)) = (Cl (Int (A /\ B))) /\ (A /\ B)
let A, B be Subset of T; ::_thesis: (Cl (Int (A /\ ((Cl (Int B)) /\ B)))) /\ (A /\ ((Cl (Int B)) /\ B)) = (Cl (Int (A /\ B))) /\ (A /\ B)
Int (A /\ B) c= Int B by TOPS_1:19, XBOOLE_1:17;
then A1: Cl (Int (A /\ B)) c= Cl (Int B) by PRE_TOPC:19;
Cl (Int (A /\ ((Cl (Int B)) /\ B))) = Cl (Int ((A /\ (Cl (Int B))) /\ B)) by XBOOLE_1:16
.= Cl ((Int (A /\ (Cl (Int B)))) /\ (Int B)) by TOPS_1:17
.= Cl (((Int A) /\ (Int (Cl (Int B)))) /\ (Int B)) by TOPS_1:17
.= Cl ((Int A) /\ ((Int (Cl (Int B))) /\ (Int B))) by XBOOLE_1:16
.= Cl ((Int A) /\ (Int B)) by Th4, XBOOLE_1:28
.= Cl (Int (A /\ B)) by TOPS_1:17 ;
then A2: Cl (Int (A /\ B)) c= (Cl (Int (A /\ ((Cl (Int B)) /\ B)))) /\ (Cl (Int B)) by A1, XBOOLE_1:19;
A /\ ((Cl (Int B)) /\ B) c= A /\ B by XBOOLE_1:17, XBOOLE_1:26;
then Int (A /\ ((Cl (Int B)) /\ B)) c= Int (A /\ B) by TOPS_1:19;
then A3: Cl (Int (A /\ ((Cl (Int B)) /\ B))) c= Cl (Int (A /\ B)) by PRE_TOPC:19;
(Cl (Int (A /\ ((Cl (Int B)) /\ B)))) /\ (Cl (Int B)) c= Cl (Int (A /\ ((Cl (Int B)) /\ B))) by XBOOLE_1:17;
then (Cl (Int (A /\ ((Cl (Int B)) /\ B)))) /\ (Cl (Int B)) c= Cl (Int (A /\ B)) by A3, XBOOLE_1:1;
then A4: (Cl (Int (A /\ ((Cl (Int B)) /\ B)))) /\ (Cl (Int B)) = Cl (Int (A /\ B)) by A2, XBOOLE_0:def_10;
A /\ ((Cl (Int B)) /\ B) = (Cl (Int B)) /\ (A /\ B) by XBOOLE_1:16;
hence (Cl (Int (A /\ ((Cl (Int B)) /\ B)))) /\ (A /\ ((Cl (Int B)) /\ B)) = (Cl (Int (A /\ B))) /\ (A /\ B) by A4, XBOOLE_1:16; ::_thesis: verum
end;
theorem :: TDLAT_1:13
for T being TopSpace
for A, C being Subset of T holds (Cl (Int (((Cl (Int A)) /\ A) /\ C))) /\ (((Cl (Int A)) /\ A) /\ C) = (Cl (Int (A /\ C))) /\ (A /\ C) by Th12;
begin
theorem Th14: :: TDLAT_1:14
for T being TopSpace holds {} T is condensed
proof
let T be TopSpace; ::_thesis: {} T is condensed
Int ({} T) c= {} T ;
then A1: Int (Cl ({} T)) c= {} T by PRE_TOPC:22;
{} T c= Cl (Int ({} T)) by PRE_TOPC:18;
hence {} T is condensed by A1, TOPS_1:def_6; ::_thesis: verum
end;
theorem Th15: :: TDLAT_1:15
for T being TopSpace holds [#] T is condensed
proof
let T be TopSpace; ::_thesis: [#] T is condensed
[#] T c= Cl ([#] T) by PRE_TOPC:18;
then A1: [#] T c= Cl (Int ([#] T)) by TOPS_1:15;
Int (Cl ([#] T)) c= [#] T ;
hence [#] T is condensed by A1, TOPS_1:def_6; ::_thesis: verum
end;
theorem Th16: :: TDLAT_1:16
for T being TopSpace
for A being Subset of T st A is condensed holds
A ` is condensed
proof
let T be TopSpace; ::_thesis: for A being Subset of T st A is condensed holds
A ` is condensed
let X be Subset of T; ::_thesis: ( X is condensed implies X ` is condensed )
assume A1: X is condensed ; ::_thesis: X ` is condensed
then X c= Cl (Int X) by TOPS_1:def_6;
then (Cl (((Int X) `) `)) ` c= X ` by SUBSET_1:12;
then Int ((Int X) `) c= X ` by TOPS_1:def_1;
then A2: Int (((Cl (X `)) `) `) c= X ` by TOPS_1:def_1;
Int (Cl X) c= X by A1, TOPS_1:def_6;
then (Cl ((Cl X) `)) ` c= X by TOPS_1:def_1;
then X ` c= Cl ((Cl ((X `) `)) `) by SUBSET_1:12;
then X ` c= Cl (Int (X `)) by TOPS_1:def_1;
hence X ` is condensed by A2, TOPS_1:def_6; ::_thesis: verum
end;
theorem Th17: :: TDLAT_1:17
for T being TopSpace
for A, B being Subset of T st A is condensed & B is condensed holds
( (Int (Cl (A \/ B))) \/ (A \/ B) is condensed & (Cl (Int (A /\ B))) /\ (A /\ B) is condensed )
proof
let T be TopSpace; ::_thesis: for A, B being Subset of T st A is condensed & B is condensed holds
( (Int (Cl (A \/ B))) \/ (A \/ B) is condensed & (Cl (Int (A /\ B))) /\ (A /\ B) is condensed )
let A, B be Subset of T; ::_thesis: ( A is condensed & B is condensed implies ( (Int (Cl (A \/ B))) \/ (A \/ B) is condensed & (Cl (Int (A /\ B))) /\ (A /\ B) is condensed ) )
assume A1: A is condensed ; ::_thesis: ( not B is condensed or ( (Int (Cl (A \/ B))) \/ (A \/ B) is condensed & (Cl (Int (A /\ B))) /\ (A /\ B) is condensed ) )
assume A2: B is condensed ; ::_thesis: ( (Int (Cl (A \/ B))) \/ (A \/ B) is condensed & (Cl (Int (A /\ B))) /\ (A /\ B) is condensed )
then A3: B c= Cl (Int B) by TOPS_1:def_6;
A4: A c= Cl (Int A) by A1, TOPS_1:def_6;
thus (Int (Cl (A \/ B))) \/ (A \/ B) is condensed ::_thesis: (Cl (Int (A /\ B))) /\ (A /\ B) is condensed
proof
set X = (Int (Cl (A \/ B))) \/ (A \/ B);
Cl ((Int A) \/ (Int B)) c= Cl (Int (A \/ B)) by PRE_TOPC:19, TOPS_1:20;
then A5: (Cl (Int A)) \/ (Cl (Int B)) c= Cl (Int (A \/ B)) by PRE_TOPC:20;
A \/ B c= (Cl (Int A)) \/ (Cl (Int B)) by A4, A3, XBOOLE_1:13;
then A \/ B c= Cl (Int (A \/ B)) by A5, XBOOLE_1:1;
then A6: (Int (Cl (A \/ B))) \/ (A \/ B) c= (Int (Cl (A \/ B))) \/ (Cl (Int (A \/ B))) by XBOOLE_1:9;
Cl ((Int (Int (Cl (A \/ B)))) \/ (Int (A \/ B))) c= Cl (Int ((Int (Cl (A \/ B))) \/ (A \/ B))) by PRE_TOPC:19, TOPS_1:20;
then A7: (Cl (Int (Cl (A \/ B)))) \/ (Cl (Int (A \/ B))) c= Cl (Int ((Int (Cl (A \/ B))) \/ (A \/ B))) by PRE_TOPC:20;
Cl (Int (Cl (A \/ B))) c= Cl (Cl (A \/ B)) by PRE_TOPC:19, TOPS_1:16;
then (Cl (Int (Cl (A \/ B)))) \/ (Cl (A \/ B)) = Cl (A \/ B) by XBOOLE_1:12;
then Int (Cl ((Int (Cl (A \/ B))) \/ (A \/ B))) = Int (Cl (A \/ B)) by PRE_TOPC:20;
then A8: Int (Cl ((Int (Cl (A \/ B))) \/ (A \/ B))) c= (Int (Cl (A \/ B))) \/ (A \/ B) by XBOOLE_1:7;
(Int (Cl (A \/ B))) \/ (Cl (Int (A \/ B))) c= (Cl (Int (Cl (A \/ B)))) \/ (Cl (Int (A \/ B))) by PRE_TOPC:18, XBOOLE_1:9;
then (Int (Cl (A \/ B))) \/ (Cl (Int (A \/ B))) c= Cl (Int ((Int (Cl (A \/ B))) \/ (A \/ B))) by A7, XBOOLE_1:1;
then (Int (Cl (A \/ B))) \/ (A \/ B) c= Cl (Int ((Int (Cl (A \/ B))) \/ (A \/ B))) by A6, XBOOLE_1:1;
hence (Int (Cl (A \/ B))) \/ (A \/ B) is condensed by A8, TOPS_1:def_6; ::_thesis: verum
end;
A9: Int (Cl B) c= B by A2, TOPS_1:def_6;
A10: Int (Cl A) c= A by A1, TOPS_1:def_6;
thus (Cl (Int (A /\ B))) /\ (A /\ B) is condensed ::_thesis: verum
proof
set X = (Cl (Int (A /\ B))) /\ (A /\ B);
Int (Cl (A /\ B)) c= Int ((Cl A) /\ (Cl B)) by PRE_TOPC:21, TOPS_1:19;
then A11: Int (Cl (A /\ B)) c= (Int (Cl A)) /\ (Int (Cl B)) by TOPS_1:17;
(Int (Cl A)) /\ (Int (Cl B)) c= A /\ B by A10, A9, XBOOLE_1:27;
then Int (Cl (A /\ B)) c= A /\ B by A11, XBOOLE_1:1;
then A12: (Cl (Int (A /\ B))) /\ (Int (Cl (A /\ B))) c= (Cl (Int (A /\ B))) /\ (A /\ B) by XBOOLE_1:26;
Int (Cl ((Cl (Int (A /\ B))) /\ (A /\ B))) c= Int ((Cl (Cl (Int (A /\ B)))) /\ (Cl (A /\ B))) by PRE_TOPC:21, TOPS_1:19;
then A13: Int (Cl ((Cl (Int (A /\ B))) /\ (A /\ B))) c= (Int (Cl (Int (A /\ B)))) /\ (Int (Cl (A /\ B))) by TOPS_1:17;
Int (Int (A /\ B)) c= Int (Cl (Int (A /\ B))) by PRE_TOPC:18, TOPS_1:19;
then Int (A /\ B) = (Int (Cl (Int (A /\ B)))) /\ (Int (A /\ B)) by XBOOLE_1:28;
then Cl (Int (A /\ B)) = Cl (Int ((Cl (Int (A /\ B))) /\ (A /\ B))) by TOPS_1:17;
then A14: (Cl (Int (A /\ B))) /\ (A /\ B) c= Cl (Int ((Cl (Int (A /\ B))) /\ (A /\ B))) by XBOOLE_1:17;
(Int (Cl (Int (A /\ B)))) /\ (Int (Cl (A /\ B))) c= (Cl (Int (A /\ B))) /\ (Int (Cl (A /\ B))) by TOPS_1:16, XBOOLE_1:26;
then Int (Cl ((Cl (Int (A /\ B))) /\ (A /\ B))) c= (Cl (Int (A /\ B))) /\ (Int (Cl (A /\ B))) by A13, XBOOLE_1:1;
then Int (Cl ((Cl (Int (A /\ B))) /\ (A /\ B))) c= (Cl (Int (A /\ B))) /\ (A /\ B) by A12, XBOOLE_1:1;
hence (Cl (Int (A /\ B))) /\ (A /\ B) is condensed by A14, TOPS_1:def_6; ::_thesis: verum
end;
end;
theorem Th18: :: TDLAT_1:18
for T being TopSpace holds {} T is closed_condensed
proof
let T be TopSpace; ::_thesis: {} T is closed_condensed
Cl (Int ({} T)) = {} T by PRE_TOPC:22;
hence {} T is closed_condensed by TOPS_1:def_7; ::_thesis: verum
end;
theorem Th19: :: TDLAT_1:19
for T being TopSpace holds [#] T is closed_condensed
proof
let T be TopSpace; ::_thesis: [#] T is closed_condensed
Int ([#] T) = [#] T by TOPS_1:15;
then Cl (Int ([#] T)) = [#] T by TOPS_1:2;
hence [#] T is closed_condensed by TOPS_1:def_7; ::_thesis: verum
end;
theorem Th20: :: TDLAT_1:20
for T being TopSpace holds {} T is open_condensed
proof
let T be TopSpace; ::_thesis: {} T is open_condensed
Cl ({} T) = {} T by PRE_TOPC:22;
then Int (Cl ({} T)) = {} T ;
hence {} T is open_condensed by TOPS_1:def_8; ::_thesis: verum
end;
theorem Th21: :: TDLAT_1:21
for T being TopSpace holds [#] T is open_condensed
proof
let T be TopSpace; ::_thesis: [#] T is open_condensed
Cl ([#] T) = [#] T by TOPS_1:2;
then Int (Cl ([#] T)) = [#] T by TOPS_1:15;
hence [#] T is open_condensed by TOPS_1:def_8; ::_thesis: verum
end;
theorem Th22: :: TDLAT_1:22
for T being TopSpace
for A being Subset of T holds Cl (Int A) is closed_condensed
proof
let T be TopSpace; ::_thesis: for A being Subset of T holds Cl (Int A) is closed_condensed
let A be Subset of T; ::_thesis: Cl (Int A) is closed_condensed
Cl (Int A) = Cl (Int (Cl (Int A))) by TOPS_1:26;
hence Cl (Int A) is closed_condensed by TOPS_1:def_7; ::_thesis: verum
end;
theorem Th23: :: TDLAT_1:23
for T being TopSpace
for A being Subset of T holds Int (Cl A) is open_condensed
proof
let T be TopSpace; ::_thesis: for A being Subset of T holds Int (Cl A) is open_condensed
let A be Subset of T; ::_thesis: Int (Cl A) is open_condensed
Int (Cl A) = Int (Cl (Int (Cl A))) by Th5;
hence Int (Cl A) is open_condensed by TOPS_1:def_8; ::_thesis: verum
end;
theorem Th24: :: TDLAT_1:24
for T being TopSpace
for A being Subset of T st A is condensed holds
Cl A is closed_condensed
proof
let T be TopSpace; ::_thesis: for A being Subset of T st A is condensed holds
Cl A is closed_condensed
let A be Subset of T; ::_thesis: ( A is condensed implies Cl A is closed_condensed )
assume A1: A is condensed ; ::_thesis: Cl A is closed_condensed
then Int (Cl A) c= A by TOPS_1:def_6;
then A2: Cl (Int (Cl A)) c= Cl A by PRE_TOPC:19;
Cl A is condensed by A1, TOPS_1:71;
then Cl A c= Cl (Int (Cl A)) by TOPS_1:def_6;
then Cl A = Cl (Int (Cl A)) by A2, XBOOLE_0:def_10;
hence Cl A is closed_condensed by TOPS_1:def_7; ::_thesis: verum
end;
theorem Th25: :: TDLAT_1:25
for T being TopSpace
for A being Subset of T st A is condensed holds
Int A is open_condensed
proof
let T be TopSpace; ::_thesis: for A being Subset of T st A is condensed holds
Int A is open_condensed
let A be Subset of T; ::_thesis: ( A is condensed implies Int A is open_condensed )
assume A1: A is condensed ; ::_thesis: Int A is open_condensed
then A c= Cl (Int A) by TOPS_1:def_6;
then A2: Int A c= Int (Cl (Int A)) by TOPS_1:19;
Int A is condensed by A1, TOPS_1:71;
then Int (Cl (Int A)) c= Int A by TOPS_1:def_6;
then Int (Cl (Int A)) = Int A by A2, XBOOLE_0:def_10;
hence Int A is open_condensed by TOPS_1:def_8; ::_thesis: verum
end;
theorem :: TDLAT_1:26
for T being TopSpace
for A being Subset of T st A is condensed holds
Cl (A `) is closed_condensed by Th16, Th24;
theorem :: TDLAT_1:27
for T being TopSpace
for A being Subset of T st A is condensed holds
Int (A `) is open_condensed by Th16, Th25;
theorem Th28: :: TDLAT_1:28
for T being TopSpace
for A, B, C being Subset of T st A is closed_condensed & B is closed_condensed & C is closed_condensed holds
Cl (Int (A /\ (Cl (Int (B /\ C))))) = Cl (Int ((Cl (Int (A /\ B))) /\ C))
proof
let T be TopSpace; ::_thesis: for A, B, C being Subset of T st A is closed_condensed & B is closed_condensed & C is closed_condensed holds
Cl (Int (A /\ (Cl (Int (B /\ C))))) = Cl (Int ((Cl (Int (A /\ B))) /\ C))
let A, B, C be Subset of T; ::_thesis: ( A is closed_condensed & B is closed_condensed & C is closed_condensed implies Cl (Int (A /\ (Cl (Int (B /\ C))))) = Cl (Int ((Cl (Int (A /\ B))) /\ C)) )
assume that
A1: A is closed_condensed and
A2: B is closed_condensed and
A3: C is closed_condensed ; ::_thesis: Cl (Int (A /\ (Cl (Int (B /\ C))))) = Cl (Int ((Cl (Int (A /\ B))) /\ C))
A4: B = Cl (Int B) by A2, TOPS_1:def_7;
A5: (A /\ B) /\ C c= C by XBOOLE_1:17;
A6: Int (A /\ (Cl (Int (B /\ C)))) c= A /\ (Cl (Int (B /\ C))) by TOPS_1:16;
A7: Cl (Int (B /\ C)) = Cl ((Int B) /\ (Int C)) by TOPS_1:17;
C = Cl (Int C) by A3, TOPS_1:def_7;
then A /\ (Cl (Int (B /\ C))) c= A /\ (B /\ C) by A7, A4, PRE_TOPC:21, XBOOLE_1:26;
then A8: Int (A /\ (Cl (Int (B /\ C)))) c= A /\ (B /\ C) by A6, XBOOLE_1:1;
then Int (A /\ (Cl (Int (B /\ C)))) c= (A /\ B) /\ C by XBOOLE_1:16;
then A9: Int (A /\ (Cl (Int (B /\ C)))) c= C by A5, XBOOLE_1:1;
A10: (A /\ B) /\ C c= A /\ B by XBOOLE_1:17;
Int (A /\ (Cl (Int (B /\ C)))) c= (A /\ B) /\ C by A8, XBOOLE_1:16;
then Int (A /\ (Cl (Int (B /\ C)))) c= A /\ B by A10, XBOOLE_1:1;
then A11: Int (Int (A /\ (Cl (Int (B /\ C))))) c= Int (A /\ B) by TOPS_1:19;
Int (A /\ B) c= Cl (Int (A /\ B)) by PRE_TOPC:18;
then Int (A /\ (Cl (Int (B /\ C)))) c= Cl (Int (A /\ B)) by A11, XBOOLE_1:1;
then Int (A /\ (Cl (Int (B /\ C)))) c= (Cl (Int (A /\ B))) /\ C by A9, XBOOLE_1:19;
then Int (Int (A /\ (Cl (Int (B /\ C))))) c= Int ((Cl (Int (A /\ B))) /\ C) by TOPS_1:19;
then A12: Cl (Int (A /\ (Cl (Int (B /\ C))))) c= Cl (Int ((Cl (Int (A /\ B))) /\ C)) by PRE_TOPC:19;
A13: A /\ (B /\ C) c= B /\ C by XBOOLE_1:17;
A14: A /\ (B /\ C) c= A by XBOOLE_1:17;
A15: Int ((Cl (Int (A /\ B))) /\ C) c= (Cl (Int (A /\ B))) /\ C by TOPS_1:16;
A16: Cl (Int (A /\ B)) = Cl ((Int A) /\ (Int B)) by TOPS_1:17;
A = Cl (Int A) by A1, TOPS_1:def_7;
then (Cl (Int (A /\ B))) /\ C c= (A /\ B) /\ C by A16, A4, PRE_TOPC:21, XBOOLE_1:26;
then A17: Int ((Cl (Int (A /\ B))) /\ C) c= (A /\ B) /\ C by A15, XBOOLE_1:1;
then Int ((Cl (Int (A /\ B))) /\ C) c= A /\ (B /\ C) by XBOOLE_1:16;
then A18: Int ((Cl (Int (A /\ B))) /\ C) c= A by A14, XBOOLE_1:1;
Int ((Cl (Int (A /\ B))) /\ C) c= A /\ (B /\ C) by A17, XBOOLE_1:16;
then Int ((Cl (Int (A /\ B))) /\ C) c= B /\ C by A13, XBOOLE_1:1;
then A19: Int (Int ((Cl (Int (A /\ B))) /\ C)) c= Int (B /\ C) by TOPS_1:19;
Int (B /\ C) c= Cl (Int (B /\ C)) by PRE_TOPC:18;
then Int ((Cl (Int (A /\ B))) /\ C) c= Cl (Int (B /\ C)) by A19, XBOOLE_1:1;
then Int ((Cl (Int (A /\ B))) /\ C) c= A /\ (Cl (Int (B /\ C))) by A18, XBOOLE_1:19;
then Int (Int ((Cl (Int (A /\ B))) /\ C)) c= Int (A /\ (Cl (Int (B /\ C)))) by TOPS_1:19;
then Cl (Int ((Cl (Int (A /\ B))) /\ C)) c= Cl (Int (A /\ (Cl (Int (B /\ C))))) by PRE_TOPC:19;
hence Cl (Int (A /\ (Cl (Int (B /\ C))))) = Cl (Int ((Cl (Int (A /\ B))) /\ C)) by A12, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th29: :: TDLAT_1:29
for T being TopSpace
for A, B, C being Subset of T st A is open_condensed & B is open_condensed & C is open_condensed holds
Int (Cl (A \/ (Int (Cl (B \/ C))))) = Int (Cl ((Int (Cl (A \/ B))) \/ C))
proof
let T be TopSpace; ::_thesis: for A, B, C being Subset of T st A is open_condensed & B is open_condensed & C is open_condensed holds
Int (Cl (A \/ (Int (Cl (B \/ C))))) = Int (Cl ((Int (Cl (A \/ B))) \/ C))
let A, B, C be Subset of T; ::_thesis: ( A is open_condensed & B is open_condensed & C is open_condensed implies Int (Cl (A \/ (Int (Cl (B \/ C))))) = Int (Cl ((Int (Cl (A \/ B))) \/ C)) )
assume that
A1: A is open_condensed and
A2: B is open_condensed and
A3: C is open_condensed ; ::_thesis: Int (Cl (A \/ (Int (Cl (B \/ C))))) = Int (Cl ((Int (Cl (A \/ B))) \/ C))
A4: B = Int (Cl B) by A2, TOPS_1:def_8;
A5: C c= (A \/ B) \/ C by XBOOLE_1:7;
A6: A \/ (Int (Cl (B \/ C))) c= Cl (A \/ (Int (Cl (B \/ C)))) by PRE_TOPC:18;
A7: Int (Cl (B \/ C)) = Int ((Cl B) \/ (Cl C)) by PRE_TOPC:20;
C = Int (Cl C) by A3, TOPS_1:def_8;
then A \/ (B \/ C) c= A \/ (Int (Cl (B \/ C))) by A7, A4, TOPS_1:20, XBOOLE_1:9;
then A8: A \/ (B \/ C) c= Cl (A \/ (Int (Cl (B \/ C)))) by A6, XBOOLE_1:1;
then (A \/ B) \/ C c= Cl (A \/ (Int (Cl (B \/ C)))) by XBOOLE_1:4;
then A9: C c= Cl (A \/ (Int (Cl (B \/ C)))) by A5, XBOOLE_1:1;
A10: A \/ B c= (A \/ B) \/ C by XBOOLE_1:7;
(A \/ B) \/ C c= Cl (A \/ (Int (Cl (B \/ C)))) by A8, XBOOLE_1:4;
then A \/ B c= Cl (A \/ (Int (Cl (B \/ C)))) by A10, XBOOLE_1:1;
then A11: Cl (A \/ B) c= Cl (Cl (A \/ (Int (Cl (B \/ C))))) by PRE_TOPC:19;
Int (Cl (A \/ B)) c= Cl (A \/ B) by TOPS_1:16;
then Int (Cl (A \/ B)) c= Cl (A \/ (Int (Cl (B \/ C)))) by A11, XBOOLE_1:1;
then (Int (Cl (A \/ B))) \/ C c= Cl (A \/ (Int (Cl (B \/ C)))) by A9, XBOOLE_1:8;
then Cl ((Int (Cl (A \/ B))) \/ C) c= Cl (Cl (A \/ (Int (Cl (B \/ C))))) by PRE_TOPC:19;
then A12: Int (Cl ((Int (Cl (A \/ B))) \/ C)) c= Int (Cl (A \/ (Int (Cl (B \/ C))))) by TOPS_1:19;
A13: B \/ C c= A \/ (B \/ C) by XBOOLE_1:7;
A14: A c= A \/ (B \/ C) by XBOOLE_1:7;
A15: (Int (Cl (A \/ B))) \/ C c= Cl ((Int (Cl (A \/ B))) \/ C) by PRE_TOPC:18;
A16: Int (Cl (A \/ B)) = Int ((Cl A) \/ (Cl B)) by PRE_TOPC:20;
A = Int (Cl A) by A1, TOPS_1:def_8;
then (A \/ B) \/ C c= (Int (Cl (A \/ B))) \/ C by A16, A4, TOPS_1:20, XBOOLE_1:9;
then A17: (A \/ B) \/ C c= Cl ((Int (Cl (A \/ B))) \/ C) by A15, XBOOLE_1:1;
then A \/ (B \/ C) c= Cl ((Int (Cl (A \/ B))) \/ C) by XBOOLE_1:4;
then A18: A c= Cl ((Int (Cl (A \/ B))) \/ C) by A14, XBOOLE_1:1;
A \/ (B \/ C) c= Cl ((Int (Cl (A \/ B))) \/ C) by A17, XBOOLE_1:4;
then B \/ C c= Cl ((Int (Cl (A \/ B))) \/ C) by A13, XBOOLE_1:1;
then A19: Cl (B \/ C) c= Cl (Cl ((Int (Cl (A \/ B))) \/ C)) by PRE_TOPC:19;
Int (Cl (B \/ C)) c= Cl (B \/ C) by TOPS_1:16;
then Int (Cl (B \/ C)) c= Cl ((Int (Cl (A \/ B))) \/ C) by A19, XBOOLE_1:1;
then A \/ (Int (Cl (B \/ C))) c= Cl ((Int (Cl (A \/ B))) \/ C) by A18, XBOOLE_1:8;
then Cl (A \/ (Int (Cl (B \/ C)))) c= Cl (Cl ((Int (Cl (A \/ B))) \/ C)) by PRE_TOPC:19;
then Int (Cl (A \/ (Int (Cl (B \/ C))))) c= Int (Cl ((Int (Cl (A \/ B))) \/ C)) by TOPS_1:19;
hence Int (Cl (A \/ (Int (Cl (B \/ C))))) = Int (Cl ((Int (Cl (A \/ B))) \/ C)) by A12, XBOOLE_0:def_10; ::_thesis: verum
end;
begin
definition
let T be TopStruct ;
func Domains_of T -> Subset-Family of T equals :: TDLAT_1:def 1
{ A where A is Subset of T : A is condensed } ;
coherence
{ A where A is Subset of T : A is condensed } is Subset-Family of T
proof
set B = { A where A is Subset of T : A is condensed } ;
{ A where A is Subset of T : A is condensed } c= bool the carrier of T
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { A where A is Subset of T : A is condensed } or x in bool the carrier of T )
assume x in { A where A is Subset of T : A is condensed } ; ::_thesis: x in bool the carrier of T
then ex A being Subset of T st
( x = A & A is condensed ) ;
hence x in bool the carrier of T ; ::_thesis: verum
end;
hence { A where A is Subset of T : A is condensed } is Subset-Family of T ; ::_thesis: verum
end;
end;
:: deftheorem defines Domains_of TDLAT_1:def_1_:_
for T being TopStruct holds Domains_of T = { A where A is Subset of T : A is condensed } ;
registration
let T be TopSpace;
cluster Domains_of T -> non empty ;
coherence
not Domains_of T is empty
proof
{} T is condensed by Th14;
then {} T in { A where A is Subset of T : A is condensed } ;
hence not Domains_of T is empty ; ::_thesis: verum
end;
end;
definition
let T be TopSpace;
func Domains_Union T -> BinOp of (Domains_of T) means :Def2: :: TDLAT_1:def 2
for A, B being Element of Domains_of T holds it . (A,B) = (Int (Cl (A \/ B))) \/ (A \/ B);
existence
ex b1 being BinOp of (Domains_of T) st
for A, B being Element of Domains_of T holds b1 . (A,B) = (Int (Cl (A \/ B))) \/ (A \/ B)
proof
defpred S1[ set , set ] means for A, B being Element of Domains_of T st $1 = [A,B] holds
$2 = (Int (Cl (A \/ B))) \/ (A \/ B);
set D = [:(Domains_of T),(Domains_of T):];
A1: for a being Element of [:(Domains_of T),(Domains_of T):] ex b being Element of Domains_of T st S1[a,b]
proof
let a be Element of [:(Domains_of T),(Domains_of T):]; ::_thesis: ex b being Element of Domains_of T st S1[a,b]
reconsider G = a `1 , F = a `2 as Element of Domains_of T ;
F in { H where H is Subset of T : H is condensed } ;
then A2: ex H being Subset of T st
( H = F & H is condensed ) ;
G in { E where E is Subset of T : E is condensed } ;
then ex E being Subset of T st
( E = G & E is condensed ) ;
then (Int (Cl (G \/ F))) \/ (G \/ F) is condensed by A2, Th17;
then (Int (Cl (G \/ F))) \/ (G \/ F) in { E where E is Subset of T : E is condensed } ;
then reconsider b = (Int (Cl (G \/ F))) \/ (G \/ F) as Element of Domains_of T ;
take b ; ::_thesis: S1[a,b]
let A, B be Element of Domains_of T; ::_thesis: ( a = [A,B] implies b = (Int (Cl (A \/ B))) \/ (A \/ B) )
assume a = [A,B] ; ::_thesis: b = (Int (Cl (A \/ B))) \/ (A \/ B)
then A3: [A,B] = [G,F] by MCART_1:21;
then A4: B = F by XTUPLE_0:1;
A = G by A3, XTUPLE_0:1;
hence b = (Int (Cl (A \/ B))) \/ (A \/ B) by A4; ::_thesis: verum
end;
consider h being Function of [:(Domains_of T),(Domains_of T):],(Domains_of T) such that
A5: for a being Element of [:(Domains_of T),(Domains_of T):] holds S1[a,h . a] from FUNCT_2:sch_3(A1);
take h ; ::_thesis: for A, B being Element of Domains_of T holds h . (A,B) = (Int (Cl (A \/ B))) \/ (A \/ B)
let A, B be Element of Domains_of T; ::_thesis: h . (A,B) = (Int (Cl (A \/ B))) \/ (A \/ B)
thus h . (A,B) = h . [A,B]
.= (Int (Cl (A \/ B))) \/ (A \/ B) by A5 ; ::_thesis: verum
end;
uniqueness
for b1, b2 being BinOp of (Domains_of T) st ( for A, B being Element of Domains_of T holds b1 . (A,B) = (Int (Cl (A \/ B))) \/ (A \/ B) ) & ( for A, B being Element of Domains_of T holds b2 . (A,B) = (Int (Cl (A \/ B))) \/ (A \/ B) ) holds
b1 = b2
proof
deffunc H1( Element of Domains_of T, Element of Domains_of T) -> Element of bool the carrier of T = (Int (Cl ($1 \/ $2))) \/ ($1 \/ $2);
thus for o1, o2 being BinOp of (Domains_of T) st ( for a, b being Element of Domains_of T holds o1 . (a,b) = H1(a,b) ) & ( for a, b being Element of Domains_of T holds o2 . (a,b) = H1(a,b) ) holds
o1 = o2 from BINOP_2:sch_2(); ::_thesis: verum
end;
end;
:: deftheorem Def2 defines Domains_Union TDLAT_1:def_2_:_
for T being TopSpace
for b2 being BinOp of (Domains_of T) holds
( b2 = Domains_Union T iff for A, B being Element of Domains_of T holds b2 . (A,B) = (Int (Cl (A \/ B))) \/ (A \/ B) );
notation
let T be TopSpace;
synonym D-Union T for Domains_Union T;
end;
definition
let T be TopSpace;
func Domains_Meet T -> BinOp of (Domains_of T) means :Def3: :: TDLAT_1:def 3
for A, B being Element of Domains_of T holds it . (A,B) = (Cl (Int (A /\ B))) /\ (A /\ B);
existence
ex b1 being BinOp of (Domains_of T) st
for A, B being Element of Domains_of T holds b1 . (A,B) = (Cl (Int (A /\ B))) /\ (A /\ B)
proof
defpred S1[ set , set ] means for A, B being Element of Domains_of T st $1 = [A,B] holds
$2 = (Cl (Int (A /\ B))) /\ (A /\ B);
set D = [:(Domains_of T),(Domains_of T):];
A1: for a being Element of [:(Domains_of T),(Domains_of T):] ex b being Element of Domains_of T st S1[a,b]
proof
let a be Element of [:(Domains_of T),(Domains_of T):]; ::_thesis: ex b being Element of Domains_of T st S1[a,b]
reconsider G = a `1 , F = a `2 as Element of Domains_of T ;
F in { H where H is Subset of T : H is condensed } ;
then A2: ex H being Subset of T st
( H = F & H is condensed ) ;
G in { E where E is Subset of T : E is condensed } ;
then ex E being Subset of T st
( E = G & E is condensed ) ;
then (Cl (Int (G /\ F))) /\ (G /\ F) is condensed by A2, Th17;
then (Cl (Int (G /\ F))) /\ (G /\ F) in { E where E is Subset of T : E is condensed } ;
then reconsider b = (Cl (Int (G /\ F))) /\ (G /\ F) as Element of Domains_of T ;
take b ; ::_thesis: S1[a,b]
let A, B be Element of Domains_of T; ::_thesis: ( a = [A,B] implies b = (Cl (Int (A /\ B))) /\ (A /\ B) )
assume a = [A,B] ; ::_thesis: b = (Cl (Int (A /\ B))) /\ (A /\ B)
then A3: [A,B] = [G,F] by MCART_1:21;
then A4: B = F by XTUPLE_0:1;
A = G by A3, XTUPLE_0:1;
hence b = (Cl (Int (A /\ B))) /\ (A /\ B) by A4; ::_thesis: verum
end;
consider h being Function of [:(Domains_of T),(Domains_of T):],(Domains_of T) such that
A5: for a being Element of [:(Domains_of T),(Domains_of T):] holds S1[a,h . a] from FUNCT_2:sch_3(A1);
take h ; ::_thesis: for A, B being Element of Domains_of T holds h . (A,B) = (Cl (Int (A /\ B))) /\ (A /\ B)
let A, B be Element of Domains_of T; ::_thesis: h . (A,B) = (Cl (Int (A /\ B))) /\ (A /\ B)
thus h . (A,B) = h . [A,B]
.= (Cl (Int (A /\ B))) /\ (A /\ B) by A5 ; ::_thesis: verum
end;
uniqueness
for b1, b2 being BinOp of (Domains_of T) st ( for A, B being Element of Domains_of T holds b1 . (A,B) = (Cl (Int (A /\ B))) /\ (A /\ B) ) & ( for A, B being Element of Domains_of T holds b2 . (A,B) = (Cl (Int (A /\ B))) /\ (A /\ B) ) holds
b1 = b2
proof
deffunc H1( Element of Domains_of T, Element of Domains_of T) -> Element of bool the carrier of T = (Cl (Int ($1 /\ $2))) /\ ($1 /\ $2);
thus for o1, o2 being BinOp of (Domains_of T) st ( for a, b being Element of Domains_of T holds o1 . (a,b) = H1(a,b) ) & ( for a, b being Element of Domains_of T holds o2 . (a,b) = H1(a,b) ) holds
o1 = o2 from BINOP_2:sch_2(); ::_thesis: verum
end;
end;
:: deftheorem Def3 defines Domains_Meet TDLAT_1:def_3_:_
for T being TopSpace
for b2 being BinOp of (Domains_of T) holds
( b2 = Domains_Meet T iff for A, B being Element of Domains_of T holds b2 . (A,B) = (Cl (Int (A /\ B))) /\ (A /\ B) );
notation
let T be TopSpace;
synonym D-Meet T for Domains_Meet T;
end;
theorem Th30: :: TDLAT_1:30
for T being TopSpace holds LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #) is C_Lattice
proof
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) #);
A1: LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #) is join-commutative
proof
let a, b be Element of LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #); :: according to LATTICES:def_4 ::_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;
A2: LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #) is meet-absorbing
proof
let a, b be Element of LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #); :: according to LATTICES:def_8 ::_thesis: (a "/\" b) "\/" b = b
reconsider A = a, B = b as Element of Domains_of T ;
A3: (Cl (Int (A /\ B))) /\ (A /\ B) c= A /\ 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 A4: Int (Cl B) c= B by TOPS_1:def_6;
A5: A /\ B c= B by XBOOLE_1:17;
a "/\" b = (Cl (Int (A /\ B))) /\ (A /\ B) by Def3;
hence (a "/\" b) "\/" b = (Int (Cl (((Cl (Int (A /\ B))) /\ (A /\ B)) \/ B))) \/ (((Cl (Int (A /\ B))) /\ (A /\ B)) \/ B) by Def2
.= (Int (Cl (((Cl (Int (A /\ B))) /\ (A /\ B)) \/ B))) \/ B by A3, A5, XBOOLE_1:1, XBOOLE_1:12
.= (Int (Cl B)) \/ B by A3, A5, XBOOLE_1:1, XBOOLE_1:12
.= b by A4, XBOOLE_1:12 ;
::_thesis: verum
end;
A6: LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #) is join-associative
proof
let a, b, c be Element of LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #); :: according to LATTICES:def_5 ::_thesis: a "\/" (b "\/" c) = (a "\/" b) "\/" c
reconsider A = a, B = b, C = c as Element of Domains_of T ;
A7: a "\/" b = (Int (Cl (A \/ B))) \/ (A \/ B) by Def2;
b "\/" c = (Int (Cl (B \/ C))) \/ (B \/ C) by Def2;
hence a "\/" (b "\/" c) = (Int (Cl (A \/ ((Int (Cl (B \/ C))) \/ (B \/ C))))) \/ (A \/ ((Int (Cl (B \/ C))) \/ (B \/ C))) by 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 A7, Def2 ;
::_thesis: verum
end;
A8: LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #) is meet-commutative
proof
let a, b be Element of LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #); :: according to LATTICES:def_6 ::_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;
A9: 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) #); :: according to LATTICES:def_9 ::_thesis: a "/\" (a "\/" b) = a
reconsider A = a, B = b as Element of Domains_of T ;
A10: A c= 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 A11: A c= Cl (Int A) by TOPS_1:def_6;
A12: A \/ B c= (Int (Cl (A \/ B))) \/ (A \/ B) by XBOOLE_1:7;
a "\/" b = (Int (Cl (A \/ B))) \/ (A \/ B) by Def2;
hence a "/\" (a "\/" b) = (Cl (Int (A /\ ((Int (Cl (A \/ B))) \/ (A \/ B))))) /\ (A /\ ((Int (Cl (A \/ B))) \/ (A \/ B))) by Def3
.= (Cl (Int (A /\ ((Int (Cl (A \/ B))) \/ (A \/ B))))) /\ A by A10, A12, XBOOLE_1:1, XBOOLE_1:28
.= (Cl (Int A)) /\ A by A10, A12, XBOOLE_1:1, XBOOLE_1:28
.= a by A11, XBOOLE_1:28 ;
::_thesis: verum
end;
LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #) is meet-associative
proof
let a, b, c be Element of LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #); :: according to LATTICES:def_7 ::_thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c
reconsider A = a, B = b, C = c as Element of Domains_of T ;
A13: a "/\" b = (Cl (Int (A /\ B))) /\ (A /\ B) by Def3;
b "/\" c = (Cl (Int (B /\ C))) /\ (B /\ C) by Def3;
hence a "/\" (b "/\" c) = (Cl (Int (A /\ ((Cl (Int (B /\ C))) /\ (B /\ C))))) /\ (A /\ ((Cl (Int (B /\ C))) /\ (B /\ C))) by 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 A13, Def3 ;
::_thesis: verum
end;
then reconsider L = LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #) as Lattice by A1, A6, A2, A8, A9;
A14: L is lower-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;
L is upper-bounded
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;
then reconsider L = L as 01_Lattice by A14;
L is complemented
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 ;
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 ;
A15: B ` misses B by XBOOLE_1:79;
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
A16: 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 A17: 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 A17, 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:2
.= c by XBOOLE_1:12
.= Top L by A16, LATTICE2:17 ; :: 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 ;
A18: 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 A19: 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 A19, XBOOLE_1:12 ; ::_thesis: verum
end;
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 A18, LATTICE2:15 ; ::_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
end;
definition
let T be TopSpace;
func Domains_Lattice T -> C_Lattice equals :: TDLAT_1:def 4
LattStr(# (Domains_of T),(Domains_Union T),(Domains_Meet T) #);
coherence
LattStr(# (Domains_of T),(Domains_Union T),(Domains_Meet T) #) is C_Lattice by Th30;
end;
:: deftheorem defines Domains_Lattice TDLAT_1:def_4_:_
for T being TopSpace holds Domains_Lattice T = LattStr(# (Domains_of T),(Domains_Union T),(Domains_Meet T) #);
begin
definition
let T be TopStruct ;
func Closed_Domains_of T -> Subset-Family of T equals :: TDLAT_1:def 5
{ A where A is Subset of T : A is closed_condensed } ;
coherence
{ A where A is Subset of T : A is closed_condensed } is Subset-Family of T
proof
set B = { A where A is Subset of T : A is closed_condensed } ;
{ A where A is Subset of T : A is closed_condensed } c= bool the carrier of T
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { A where A is Subset of T : A is closed_condensed } or x in bool the carrier of T )
assume x in { A where A is Subset of T : A is closed_condensed } ; ::_thesis: x in bool the carrier of T
then ex A being Subset of T st
( x = A & A is closed_condensed ) ;
hence x in bool the carrier of T ; ::_thesis: verum
end;
hence { A where A is Subset of T : A is closed_condensed } is Subset-Family of T ; ::_thesis: verum
end;
end;
:: deftheorem defines Closed_Domains_of TDLAT_1:def_5_:_
for T being TopStruct holds Closed_Domains_of T = { A where A is Subset of T : A is closed_condensed } ;
registration
let T be TopSpace;
cluster Closed_Domains_of T -> non empty ;
coherence
not Closed_Domains_of T is empty
proof
{} T is closed_condensed by Th18;
then {} T in { A where A is Subset of T : A is closed_condensed } ;
hence not Closed_Domains_of T is empty ; ::_thesis: verum
end;
end;
theorem :: TDLAT_1:31
for T being TopSpace holds Closed_Domains_of T c= Domains_of T ;
definition
let T be TopSpace;
func Closed_Domains_Union T -> BinOp of (Closed_Domains_of T) means :Def6: :: TDLAT_1:def 6
for A, B being Element of Closed_Domains_of T holds it . (A,B) = A \/ B;
existence
ex b1 being BinOp of (Closed_Domains_of T) st
for A, B being Element of Closed_Domains_of T holds b1 . (A,B) = A \/ B
proof
defpred S1[ set , set ] means for A, B being Element of Closed_Domains_of T st $1 = [A,B] holds
$2 = A \/ B;
set D = [:(Closed_Domains_of T),(Closed_Domains_of T):];
A1: for a being Element of [:(Closed_Domains_of T),(Closed_Domains_of T):] ex b being Element of Closed_Domains_of T st S1[a,b]
proof
let a be Element of [:(Closed_Domains_of T),(Closed_Domains_of T):]; ::_thesis: ex b being Element of Closed_Domains_of T st S1[a,b]
reconsider G = a `1 , F = a `2 as Element of Closed_Domains_of T ;
G in { E where E is Subset of T : E is closed_condensed } ;
then consider E being Subset of T such that
A2: E = G and
A3: E is closed_condensed ;
F in { H where H is Subset of T : H is closed_condensed } ;
then consider H being Subset of T such that
A4: H = F and
A5: H is closed_condensed ;
E \/ H is closed_condensed by A3, A5, TOPS_1:68;
then G \/ F in { K where K is Subset of T : K is closed_condensed } by A2, A4;
then reconsider b = G \/ F as Element of Closed_Domains_of T ;
take b ; ::_thesis: S1[a,b]
let A, B be Element of Closed_Domains_of T; ::_thesis: ( a = [A,B] implies b = A \/ B )
assume a = [A,B] ; ::_thesis: b = A \/ B
then A6: [A,B] = [G,F] by MCART_1:21;
then A = G by XTUPLE_0:1;
hence b = A \/ B by A6, XTUPLE_0:1; ::_thesis: verum
end;
consider h being Function of [:(Closed_Domains_of T),(Closed_Domains_of T):],(Closed_Domains_of T) such that
A7: for a being Element of [:(Closed_Domains_of T),(Closed_Domains_of T):] holds S1[a,h . a] from FUNCT_2:sch_3(A1);
take h ; ::_thesis: for A, B being Element of Closed_Domains_of T holds h . (A,B) = A \/ B
let A, B be Element of Closed_Domains_of T; ::_thesis: h . (A,B) = A \/ B
thus h . (A,B) = h . [A,B]
.= A \/ B by A7 ; ::_thesis: verum
end;
uniqueness
for b1, b2 being BinOp of (Closed_Domains_of T) st ( for A, B being Element of Closed_Domains_of T holds b1 . (A,B) = A \/ B ) & ( for A, B being Element of Closed_Domains_of T holds b2 . (A,B) = A \/ B ) holds
b1 = b2
proof
deffunc H1( Element of Closed_Domains_of T, Element of Closed_Domains_of T) -> Element of bool the carrier of T = $1 \/ $2;
thus for o1, o2 being BinOp of (Closed_Domains_of T) st ( for a, b being Element of Closed_Domains_of T holds o1 . (a,b) = H1(a,b) ) & ( for a, b being Element of Closed_Domains_of T holds o2 . (a,b) = H1(a,b) ) holds
o1 = o2 from BINOP_2:sch_2(); ::_thesis: verum
end;
end;
:: deftheorem Def6 defines Closed_Domains_Union TDLAT_1:def_6_:_
for T being TopSpace
for b2 being BinOp of (Closed_Domains_of T) holds
( b2 = Closed_Domains_Union T iff for A, B being Element of Closed_Domains_of T holds b2 . (A,B) = A \/ B );
notation
let T be TopSpace;
synonym CLD-Union T for Closed_Domains_Union T;
end;
theorem Th32: :: TDLAT_1:32
for T being TopSpace
for A, B being Element of Closed_Domains_of T holds (CLD-Union T) . (A,B) = (D-Union T) . (A,B)
proof
let T be TopSpace; ::_thesis: for A, B being Element of Closed_Domains_of T holds (CLD-Union T) . (A,B) = (D-Union T) . (A,B)
let A, B be Element of Closed_Domains_of T; ::_thesis: (CLD-Union T) . (A,B) = (D-Union T) . (A,B)
A1: A in { D where D is Subset of T : D is closed_condensed } ;
reconsider A0 = A, B0 = B as Element of Domains_of T ;
B in { E where E is Subset of T : E is closed_condensed } ;
then consider E being Subset of T such that
A2: E = B and
A3: E is closed_condensed ;
consider D being Subset of T such that
A4: D = A and
A5: D is closed_condensed by A1;
D \/ E is closed_condensed by A5, A3, TOPS_1:68;
then D \/ E is condensed by TOPS_1:66;
then A6: Int (Cl (A \/ B)) c= A \/ B by A4, A2, TOPS_1:def_6;
thus (CLD-Union T) . (A,B) = A \/ B by Def6
.= (Int (Cl (A0 \/ B0))) \/ (A0 \/ B0) by A6, XBOOLE_1:12
.= (D-Union T) . (A,B) by Def2 ; ::_thesis: verum
end;
definition
let T be TopSpace;
func Closed_Domains_Meet T -> BinOp of (Closed_Domains_of T) means :Def7: :: TDLAT_1:def 7
for A, B being Element of Closed_Domains_of T holds it . (A,B) = Cl (Int (A /\ B));
existence
ex b1 being BinOp of (Closed_Domains_of T) st
for A, B being Element of Closed_Domains_of T holds b1 . (A,B) = Cl (Int (A /\ B))
proof
defpred S1[ set , set ] means for A, B being Element of Closed_Domains_of T st $1 = [A,B] holds
$2 = Cl (Int (A /\ B));
set D = [:(Closed_Domains_of T),(Closed_Domains_of T):];
A1: for a being Element of [:(Closed_Domains_of T),(Closed_Domains_of T):] ex b being Element of Closed_Domains_of T st S1[a,b]
proof
let a be Element of [:(Closed_Domains_of T),(Closed_Domains_of T):]; ::_thesis: ex b being Element of Closed_Domains_of T st S1[a,b]
reconsider G = a `1 , F = a `2 as Element of Closed_Domains_of T ;
Cl (Int (G /\ F)) is closed_condensed by Th22;
then Cl (Int (G /\ F)) in { E where E is Subset of T : E is closed_condensed } ;
then reconsider b = Cl (Int (G /\ F)) as Element of Closed_Domains_of T ;
take b ; ::_thesis: S1[a,b]
let A, B be Element of Closed_Domains_of T; ::_thesis: ( a = [A,B] implies b = Cl (Int (A /\ B)) )
assume a = [A,B] ; ::_thesis: b = Cl (Int (A /\ B))
then A2: [A,B] = [G,F] by MCART_1:21;
then A = G by XTUPLE_0:1;
hence b = Cl (Int (A /\ B)) by A2, XTUPLE_0:1; ::_thesis: verum
end;
consider h being Function of [:(Closed_Domains_of T),(Closed_Domains_of T):],(Closed_Domains_of T) such that
A3: for a being Element of [:(Closed_Domains_of T),(Closed_Domains_of T):] holds S1[a,h . a] from FUNCT_2:sch_3(A1);
take h ; ::_thesis: for A, B being Element of Closed_Domains_of T holds h . (A,B) = Cl (Int (A /\ B))
let A, B be Element of Closed_Domains_of T; ::_thesis: h . (A,B) = Cl (Int (A /\ B))
thus h . (A,B) = h . [A,B]
.= Cl (Int (A /\ B)) by A3 ; ::_thesis: verum
end;
uniqueness
for b1, b2 being BinOp of (Closed_Domains_of T) st ( for A, B being Element of Closed_Domains_of T holds b1 . (A,B) = Cl (Int (A /\ B)) ) & ( for A, B being Element of Closed_Domains_of T holds b2 . (A,B) = Cl (Int (A /\ B)) ) holds
b1 = b2
proof
deffunc H1( Element of Closed_Domains_of T, Element of Closed_Domains_of T) -> Element of bool the carrier of T = Cl (Int ($1 /\ $2));
thus for o1, o2 being BinOp of (Closed_Domains_of T) st ( for a, b being Element of Closed_Domains_of T holds o1 . (a,b) = H1(a,b) ) & ( for a, b being Element of Closed_Domains_of T holds o2 . (a,b) = H1(a,b) ) holds
o1 = o2 from BINOP_2:sch_2(); ::_thesis: verum
end;
end;
:: deftheorem Def7 defines Closed_Domains_Meet TDLAT_1:def_7_:_
for T being TopSpace
for b2 being BinOp of (Closed_Domains_of T) holds
( b2 = Closed_Domains_Meet T iff for A, B being Element of Closed_Domains_of T holds b2 . (A,B) = Cl (Int (A /\ B)) );
notation
let T be TopSpace;
synonym CLD-Meet T for Closed_Domains_Meet T;
end;
theorem Th33: :: TDLAT_1:33
for T being TopSpace
for A, B being Element of Closed_Domains_of T holds (CLD-Meet T) . (A,B) = (D-Meet T) . (A,B)
proof
let T be TopSpace; ::_thesis: for A, B being Element of Closed_Domains_of T holds (CLD-Meet T) . (A,B) = (D-Meet T) . (A,B)
let A, B be Element of Closed_Domains_of T; ::_thesis: (CLD-Meet T) . (A,B) = (D-Meet T) . (A,B)
A in { D where D is Subset of T : D is closed_condensed } ;
then consider D being Subset of T such that
A1: D = A and
A2: D is closed_condensed ;
A3: Int (A /\ B) c= A /\ B by TOPS_1:16;
reconsider A0 = A, B0 = B as Element of Domains_of T ;
B in { E where E is Subset of T : E is closed_condensed } ;
then consider E being Subset of T such that
A4: E = B and
A5: E is closed_condensed ;
A6: E is closed by A5, TOPS_1:66;
D is closed by A2, TOPS_1:66;
then A7: Cl (D /\ E) = D /\ E by A6, PRE_TOPC:22;
thus (CLD-Meet T) . (A,B) = Cl (Int (A /\ B)) by Def7
.= (Cl (Int (A0 /\ B0))) /\ (A0 /\ B0) by A1, A4, A7, A3, PRE_TOPC:19, XBOOLE_1:28
.= (D-Meet T) . (A,B) by Def3 ; ::_thesis: verum
end;
theorem Th34: :: TDLAT_1:34
for T being TopSpace holds LattStr(# (Closed_Domains_of T),(CLD-Union T),(CLD-Meet T) #) is B_Lattice
proof
let T be TopSpace; ::_thesis: LattStr(# (Closed_Domains_of T),(CLD-Union T),(CLD-Meet T) #) is B_Lattice
set L = LattStr(# (Closed_Domains_of T),(CLD-Union T),(CLD-Meet T) #);
A1: LattStr(# (Closed_Domains_of T),(CLD-Union T),(CLD-Meet T) #) is join-commutative
proof
let a, b be Element of LattStr(# (Closed_Domains_of T),(CLD-Union T),(CLD-Meet T) #); :: according to LATTICES:def_4 ::_thesis: a "\/" b = b "\/" a
reconsider A = a, B = b as Element of Closed_Domains_of T ;
thus a "\/" b = B \/ A by Def6
.= b "\/" a by Def6 ; ::_thesis: verum
end;
A2: LattStr(# (Closed_Domains_of T),(CLD-Union T),(CLD-Meet T) #) is meet-absorbing
proof
let a, b be Element of LattStr(# (Closed_Domains_of T),(CLD-Union T),(CLD-Meet T) #); :: according to LATTICES:def_8 ::_thesis: (a "/\" b) "\/" b = b
reconsider A = a, B = b as Element of Closed_Domains_of T ;
A3: (Cl (Int A)) /\ B c= B by XBOOLE_1:17;
B in { D where D is Subset of T : D is closed_condensed } ;
then ex D being Subset of T st
( D = B & D is closed_condensed ) ;
then A4: B = Cl (Int B) by TOPS_1:def_7;
Cl (Int (A /\ B)) = Cl ((Int A) /\ (Int B)) by TOPS_1:17;
then A5: Cl (Int (A /\ B)) c= (Cl (Int A)) /\ B by A4, PRE_TOPC:21;
a "/\" b = Cl (Int (A /\ B)) by Def7;
hence (a "/\" b) "\/" b = (Cl (Int (A /\ B))) \/ B by Def6
.= b by A5, A3, XBOOLE_1:1, XBOOLE_1:12 ;
::_thesis: verum
end;
A6: LattStr(# (Closed_Domains_of T),(CLD-Union T),(CLD-Meet T) #) is join-absorbing
proof
let a, b be Element of LattStr(# (Closed_Domains_of T),(CLD-Union T),(CLD-Meet T) #); :: according to LATTICES:def_9 ::_thesis: a "/\" (a "\/" b) = a
reconsider A = a, B = b as Element of Closed_Domains_of T ;
A in { D where D is Subset of T : D is closed_condensed } ;
then A7: ex D being Subset of T st
( D = A & D is closed_condensed ) ;
a "\/" b = A \/ B by Def6;
hence a "/\" (a "\/" b) = Cl (Int (A /\ (A \/ B))) by Def7
.= Cl (Int A) by XBOOLE_1:21
.= a by A7, TOPS_1:def_7 ;
::_thesis: verum
end;
A8: LattStr(# (Closed_Domains_of T),(CLD-Union T),(CLD-Meet T) #) is join-associative
proof
let a, b, c be Element of LattStr(# (Closed_Domains_of T),(CLD-Union T),(CLD-Meet T) #); :: according to LATTICES:def_5 ::_thesis: a "\/" (b "\/" c) = (a "\/" b) "\/" c
reconsider A = a, B = b, C = c as Element of Closed_Domains_of T ;
A9: a "\/" b = A \/ B by Def6;
b "\/" c = B \/ C by Def6;
hence a "\/" (b "\/" c) = A \/ (B \/ C) by Def6
.= (A \/ B) \/ C by XBOOLE_1:4
.= (a "\/" b) "\/" c by A9, Def6 ;
::_thesis: verum
end;
A10: LattStr(# (Closed_Domains_of T),(CLD-Union T),(CLD-Meet T) #) is meet-associative
proof
let a, b, c be Element of LattStr(# (Closed_Domains_of T),(CLD-Union T),(CLD-Meet T) #); :: according to LATTICES:def_7 ::_thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c
reconsider A = a, B = b, C = c as Element of Closed_Domains_of T ;
A in { D where D is Subset of T : D is closed_condensed } ;
then A11: ex D being Subset of T st
( D = A & D is closed_condensed ) ;
B in { E where E is Subset of T : E is closed_condensed } ;
then A12: ex E being Subset of T st
( E = B & E is closed_condensed ) ;
C in { F where F is Subset of T : F is closed_condensed } ;
then A13: ex F being Subset of T st
( F = C & F is closed_condensed ) ;
A14: a "/\" b = Cl (Int (A /\ B)) by Def7;
b "/\" c = Cl (Int (B /\ C)) by Def7;
hence a "/\" (b "/\" c) = Cl (Int (A /\ (Cl (Int (B /\ C))))) by Def7
.= Cl (Int ((Cl (Int (A /\ B))) /\ C)) by A11, A12, A13, Th28
.= (a "/\" b) "/\" c by A14, Def7 ;
::_thesis: verum
end;
LattStr(# (Closed_Domains_of T),(CLD-Union T),(CLD-Meet T) #) is meet-commutative
proof
let a, b be Element of LattStr(# (Closed_Domains_of T),(CLD-Union T),(CLD-Meet T) #); :: according to LATTICES:def_6 ::_thesis: a "/\" b = b "/\" a
reconsider A = a, B = b as Element of Closed_Domains_of T ;
thus a "/\" b = Cl (Int (B /\ A)) by Def7
.= b "/\" a by Def7 ; ::_thesis: verum
end;
then reconsider L = LattStr(# (Closed_Domains_of T),(CLD-Union T),(CLD-Meet T) #) as Lattice by A1, A8, A2, A10, A6;
A15: L is upper-bounded
proof
[#] T is closed_condensed by Th19;
then [#] T in { D where D is Subset of T : D is closed_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 Closed_Domains_of T ;
thus c "\/" a = C \/ A by Def6
.= c by XBOOLE_1:12 ; ::_thesis: a "\/" c = c
hence a "\/" c = c ; ::_thesis: verum
end;
A16: L is distributive
proof
let a, b, c be Element of L; :: according to LATTICES:def_11 ::_thesis: a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c)
reconsider A = a, B = b, C = c as Element of Closed_Domains_of T ;
A in { D where D is Subset of T : D is closed_condensed } ;
then consider D being Subset of T such that
A17: D = A and
A18: D is closed_condensed ;
A19: D is closed by A18, TOPS_1:66;
B in { E where E is Subset of T : E is closed_condensed } ;
then consider E being Subset of T such that
A20: E = B and
A21: E is closed_condensed ;
A22: E is closed by A21, TOPS_1:66;
A23: a "/\" c = Cl (Int (A /\ C)) by Def7;
A24: a "/\" b = Cl (Int (A /\ B)) by Def7;
b "\/" c = B \/ C by Def6;
hence a "/\" (b "\/" c) = Cl (Int (A /\ (B \/ C))) by Def7
.= Cl (Int ((A /\ B) \/ (A /\ C))) by XBOOLE_1:23
.= (Cl (Int (A /\ B))) \/ (Cl (Int (A /\ C))) by A17, A20, A19, A22, Th6
.= (a "/\" b) "\/" (a "/\" c) by A24, A23, Def6 ;
::_thesis: verum
end;
A25: L is complemented
proof
[#] T is closed_condensed by Th19;
then [#] T in { K where K is Subset of T : K is closed_condensed } ;
then reconsider c = [#] T as Element of L ;
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 Closed_Domains_of T ;
B in { D where D is Subset of T : D is closed_condensed } ;
then consider D being Subset of T such that
A26: D = B and
A27: D is closed_condensed ;
D is condensed by A27, TOPS_1:66;
then Cl (B `) is closed_condensed by A26, Th16, Th24;
then Cl (B `) in { K where K is Subset of T : K is closed_condensed } ;
then reconsider a = Cl (B `) as Element of L ;
take a ; ::_thesis: a is_a_complement_of b
A28: D is closed by A27, TOPS_1:66;
A29: 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 Closed_Domains_of T ;
V in { K where K is Subset of T : K is closed_condensed } ;
then A30: ex D being Subset of T st
( D = V & D is closed_condensed ) ;
thus the L_meet of L . (c,v) = Cl (Int (([#] T) /\ V)) by Def7
.= Cl (Int V) by XBOOLE_1:28
.= v by A30, TOPS_1:def_7 ; ::_thesis: verum
end;
thus a "\/" b = (Cl (B `)) \/ B by Def6
.= (Cl (D `)) \/ (Cl D) by A26, A28, PRE_TOPC:22
.= Cl ((B `) \/ B) by A26, PRE_TOPC:20
.= Cl ([#] T) by PRE_TOPC:2
.= c by TOPS_1:2
.= Top L by A29, LATTICE2:17 ; :: 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 closed_condensed by Th18;
then {} T in { K where K is Subset of T : K is closed_condensed } ;
then reconsider c = {} T as Element of L ;
A31: 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 Closed_Domains_of T ;
thus the L_join of L . (c,v) = ({} T) \/ V by Def6
.= (([#] T) `) \/ ((V `) `) by XBOOLE_1:37
.= (([#] T) /\ (V `)) ` by XBOOLE_1:54
.= (V `) ` by XBOOLE_1:28
.= v ; ::_thesis: verum
end;
thus a "/\" b = Cl (Int (B /\ (Cl (B `)))) by Def7
.= Cl ({} T) by Th8
.= c by PRE_TOPC:22
.= Bottom L by A31, LATTICE2:15 ; ::_thesis: b "/\" a = Bottom L
hence b "/\" a = Bottom L ; ::_thesis: verum
end;
L is lower-bounded
proof
A32: {} T is closed_condensed by Th18;
then {} T in { D where D is Subset of T : D is closed_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 Closed_Domains_of T ;
thus c "/\" a = Cl (Int (C /\ A)) by Def7
.= c by A32, TOPS_1:def_7 ; ::_thesis: a "/\" c = c
hence a "/\" c = c ; ::_thesis: verum
end;
hence LattStr(# (Closed_Domains_of T),(CLD-Union T),(CLD-Meet T) #) is B_Lattice by A15, A25, A16; ::_thesis: verum
end;
definition
let T be TopSpace;
func Closed_Domains_Lattice T -> B_Lattice equals :: TDLAT_1:def 8
LattStr(# (Closed_Domains_of T),(Closed_Domains_Union T),(Closed_Domains_Meet T) #);
coherence
LattStr(# (Closed_Domains_of T),(Closed_Domains_Union T),(Closed_Domains_Meet T) #) is B_Lattice by Th34;
end;
:: deftheorem defines Closed_Domains_Lattice TDLAT_1:def_8_:_
for T being TopSpace holds Closed_Domains_Lattice T = LattStr(# (Closed_Domains_of T),(Closed_Domains_Union T),(Closed_Domains_Meet T) #);
begin
definition
let T be TopStruct ;
func Open_Domains_of T -> Subset-Family of T equals :: TDLAT_1:def 9
{ A where A is Subset of T : A is open_condensed } ;
coherence
{ A where A is Subset of T : A is open_condensed } is Subset-Family of T
proof
set B = { A where A is Subset of T : A is open_condensed } ;
{ A where A is Subset of T : A is open_condensed } c= bool the carrier of T
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { A where A is Subset of T : A is open_condensed } or x in bool the carrier of T )
assume x in { A where A is Subset of T : A is open_condensed } ; ::_thesis: x in bool the carrier of T
then ex A being Subset of T st
( x = A & A is open_condensed ) ;
hence x in bool the carrier of T ; ::_thesis: verum
end;
hence { A where A is Subset of T : A is open_condensed } is Subset-Family of T ; ::_thesis: verum
end;
end;
:: deftheorem defines Open_Domains_of TDLAT_1:def_9_:_
for T being TopStruct holds Open_Domains_of T = { A where A is Subset of T : A is open_condensed } ;
registration
let T be TopSpace;
cluster Open_Domains_of T -> non empty ;
coherence
not Open_Domains_of T is empty
proof
{} T is open_condensed by Th20;
then {} T in { A where A is Subset of T : A is open_condensed } ;
hence not Open_Domains_of T is empty ; ::_thesis: verum
end;
end;
theorem :: TDLAT_1:35
for T being TopSpace holds Open_Domains_of T c= Domains_of T ;
definition
let T be TopSpace;
func Open_Domains_Union T -> BinOp of (Open_Domains_of T) means :Def10: :: TDLAT_1:def 10
for A, B being Element of Open_Domains_of T holds it . (A,B) = Int (Cl (A \/ B));
existence
ex b1 being BinOp of (Open_Domains_of T) st
for A, B being Element of Open_Domains_of T holds b1 . (A,B) = Int (Cl (A \/ B))
proof
defpred S1[ set , set ] means for A, B being Element of Open_Domains_of T st $1 = [A,B] holds
$2 = Int (Cl (A \/ B));
set D = [:(Open_Domains_of T),(Open_Domains_of T):];
A1: for a being Element of [:(Open_Domains_of T),(Open_Domains_of T):] ex b being Element of Open_Domains_of T st S1[a,b]
proof
let a be Element of [:(Open_Domains_of T),(Open_Domains_of T):]; ::_thesis: ex b being Element of Open_Domains_of T st S1[a,b]
reconsider G = a `1 , F = a `2 as Element of Open_Domains_of T ;
Int (Cl (G \/ F)) is open_condensed by Th23;
then Int (Cl (G \/ F)) in { E where E is Subset of T : E is open_condensed } ;
then reconsider b = Int (Cl (G \/ F)) as Element of Open_Domains_of T ;
take b ; ::_thesis: S1[a,b]
let A, B be Element of Open_Domains_of T; ::_thesis: ( a = [A,B] implies b = Int (Cl (A \/ B)) )
assume a = [A,B] ; ::_thesis: b = Int (Cl (A \/ B))
then A2: [A,B] = [G,F] by MCART_1:21;
then A = G by XTUPLE_0:1;
hence b = Int (Cl (A \/ B)) by A2, XTUPLE_0:1; ::_thesis: verum
end;
consider h being Function of [:(Open_Domains_of T),(Open_Domains_of T):],(Open_Domains_of T) such that
A3: for a being Element of [:(Open_Domains_of T),(Open_Domains_of T):] holds S1[a,h . a] from FUNCT_2:sch_3(A1);
take h ; ::_thesis: for A, B being Element of Open_Domains_of T holds h . (A,B) = Int (Cl (A \/ B))
let A, B be Element of Open_Domains_of T; ::_thesis: h . (A,B) = Int (Cl (A \/ B))
thus h . (A,B) = h . [A,B]
.= Int (Cl (A \/ B)) by A3 ; ::_thesis: verum
end;
uniqueness
for b1, b2 being BinOp of (Open_Domains_of T) st ( for A, B being Element of Open_Domains_of T holds b1 . (A,B) = Int (Cl (A \/ B)) ) & ( for A, B being Element of Open_Domains_of T holds b2 . (A,B) = Int (Cl (A \/ B)) ) holds
b1 = b2
proof
deffunc H1( Element of Open_Domains_of T, Element of Open_Domains_of T) -> Element of bool the carrier of T = Int (Cl ($1 \/ $2));
thus for o1, o2 being BinOp of (Open_Domains_of T) st ( for a, b being Element of Open_Domains_of T holds o1 . (a,b) = H1(a,b) ) & ( for a, b being Element of Open_Domains_of T holds o2 . (a,b) = H1(a,b) ) holds
o1 = o2 from BINOP_2:sch_2(); ::_thesis: verum
end;
end;
:: deftheorem Def10 defines Open_Domains_Union TDLAT_1:def_10_:_
for T being TopSpace
for b2 being BinOp of (Open_Domains_of T) holds
( b2 = Open_Domains_Union T iff for A, B being Element of Open_Domains_of T holds b2 . (A,B) = Int (Cl (A \/ B)) );
notation
let T be TopSpace;
synonym OPD-Union T for Open_Domains_Union T;
end;
theorem Th36: :: TDLAT_1:36
for T being TopSpace
for A, B being Element of Open_Domains_of T holds (OPD-Union T) . (A,B) = (D-Union T) . (A,B)
proof
let T be TopSpace; ::_thesis: for A, B being Element of Open_Domains_of T holds (OPD-Union T) . (A,B) = (D-Union T) . (A,B)
let A, B be Element of Open_Domains_of T; ::_thesis: (OPD-Union T) . (A,B) = (D-Union T) . (A,B)
A in { D where D is Subset of T : D is open_condensed } ;
then consider D being Subset of T such that
A1: D = A and
A2: D is open_condensed ;
A3: A \/ B c= Cl (A \/ B) by PRE_TOPC:18;
reconsider A0 = A, B0 = B as Element of Domains_of T ;
B in { E where E is Subset of T : E is open_condensed } ;
then consider E being Subset of T such that
A4: E = B and
A5: E is open_condensed ;
A6: E is open by A5, TOPS_1:67;
D is open by A2, TOPS_1:67;
then A7: Int (D \/ E) = D \/ E by A6, TOPS_1:23;
thus (OPD-Union T) . (A,B) = Int (Cl (A \/ B)) by Def10
.= (Int (Cl (A0 \/ B0))) \/ (A0 \/ B0) by A1, A4, A7, A3, TOPS_1:19, XBOOLE_1:12
.= (D-Union T) . (A,B) by Def2 ; ::_thesis: verum
end;
definition
let T be TopSpace;
func Open_Domains_Meet T -> BinOp of (Open_Domains_of T) means :Def11: :: TDLAT_1:def 11
for A, B being Element of Open_Domains_of T holds it . (A,B) = A /\ B;
existence
ex b1 being BinOp of (Open_Domains_of T) st
for A, B being Element of Open_Domains_of T holds b1 . (A,B) = A /\ B
proof
defpred S1[ set , set ] means for A, B being Element of Open_Domains_of T st $1 = [A,B] holds
$2 = A /\ B;
set D = [:(Open_Domains_of T),(Open_Domains_of T):];
A1: for a being Element of [:(Open_Domains_of T),(Open_Domains_of T):] ex b being Element of Open_Domains_of T st S1[a,b]
proof
let a be Element of [:(Open_Domains_of T),(Open_Domains_of T):]; ::_thesis: ex b being Element of Open_Domains_of T st S1[a,b]
reconsider G = a `1 , F = a `2 as Element of Open_Domains_of T ;
G in { E where E is Subset of T : E is open_condensed } ;
then consider E being Subset of T such that
A2: E = G and
A3: E is open_condensed ;
F in { H where H is Subset of T : H is open_condensed } ;
then consider H being Subset of T such that
A4: H = F and
A5: H is open_condensed ;
E /\ H is open_condensed by A3, A5, TOPS_1:69;
then G /\ F in { K where K is Subset of T : K is open_condensed } by A2, A4;
then reconsider b = G /\ F as Element of Open_Domains_of T ;
take b ; ::_thesis: S1[a,b]
let A, B be Element of Open_Domains_of T; ::_thesis: ( a = [A,B] implies b = A /\ B )
assume a = [A,B] ; ::_thesis: b = A /\ B
then A6: [A,B] = [G,F] by MCART_1:21;
then A = G by XTUPLE_0:1;
hence b = A /\ B by A6, XTUPLE_0:1; ::_thesis: verum
end;
consider h being Function of [:(Open_Domains_of T),(Open_Domains_of T):],(Open_Domains_of T) such that
A7: for a being Element of [:(Open_Domains_of T),(Open_Domains_of T):] holds S1[a,h . a] from FUNCT_2:sch_3(A1);
take h ; ::_thesis: for A, B being Element of Open_Domains_of T holds h . (A,B) = A /\ B
let A, B be Element of Open_Domains_of T; ::_thesis: h . (A,B) = A /\ B
thus h . (A,B) = h . [A,B]
.= A /\ B by A7 ; ::_thesis: verum
end;
uniqueness
for b1, b2 being BinOp of (Open_Domains_of T) st ( for A, B being Element of Open_Domains_of T holds b1 . (A,B) = A /\ B ) & ( for A, B being Element of Open_Domains_of T holds b2 . (A,B) = A /\ B ) holds
b1 = b2
proof
deffunc H1( Element of Open_Domains_of T, Element of Open_Domains_of T) -> Element of bool the carrier of T = $1 /\ $2;
thus for o1, o2 being BinOp of (Open_Domains_of T) st ( for a, b being Element of Open_Domains_of T holds o1 . (a,b) = H1(a,b) ) & ( for a, b being Element of Open_Domains_of T holds o2 . (a,b) = H1(a,b) ) holds
o1 = o2 from BINOP_2:sch_2(); ::_thesis: verum
end;
end;
:: deftheorem Def11 defines Open_Domains_Meet TDLAT_1:def_11_:_
for T being TopSpace
for b2 being BinOp of (Open_Domains_of T) holds
( b2 = Open_Domains_Meet T iff for A, B being Element of Open_Domains_of T holds b2 . (A,B) = A /\ B );
notation
let T be TopSpace;
synonym OPD-Meet T for Open_Domains_Meet T;
end;
theorem Th37: :: TDLAT_1:37
for T being TopSpace
for A, B being Element of Open_Domains_of T holds (OPD-Meet T) . (A,B) = (D-Meet T) . (A,B)
proof
let T be TopSpace; ::_thesis: for A, B being Element of Open_Domains_of T holds (OPD-Meet T) . (A,B) = (D-Meet T) . (A,B)
let A, B be Element of Open_Domains_of T; ::_thesis: (OPD-Meet T) . (A,B) = (D-Meet T) . (A,B)
A1: A in { D where D is Subset of T : D is open_condensed } ;
reconsider A0 = A, B0 = B as Element of Domains_of T ;
B in { E where E is Subset of T : E is open_condensed } ;
then consider E being Subset of T such that
A2: E = B and
A3: E is open_condensed ;
consider D being Subset of T such that
A4: D = A and
A5: D is open_condensed by A1;
D /\ E is open_condensed by A5, A3, TOPS_1:69;
then A /\ B is condensed by A4, A2, TOPS_1:67;
then A6: A /\ B c= Cl (Int (A /\ B)) by TOPS_1:def_6;
thus (OPD-Meet T) . (A,B) = A /\ B by Def11
.= (Cl (Int (A0 /\ B0))) /\ (A0 /\ B0) by A6, XBOOLE_1:28
.= (D-Meet T) . (A,B) by Def3 ; ::_thesis: verum
end;
theorem Th38: :: TDLAT_1:38
for T being TopSpace holds LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #) is B_Lattice
proof
let T be TopSpace; ::_thesis: LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #) is B_Lattice
set L = LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #);
A1: LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #) is join-commutative
proof
let a, b be Element of LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #); :: according to LATTICES:def_4 ::_thesis: a "\/" b = b "\/" a
reconsider A = a, B = b as Element of Open_Domains_of T ;
thus a "\/" b = Int (Cl (B \/ A)) by Def10
.= b "\/" a by Def10 ; ::_thesis: verum
end;
A2: LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #) is meet-absorbing
proof
let a, b be Element of LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #); :: according to LATTICES:def_8 ::_thesis: (a "/\" b) "\/" b = b
reconsider A = a, B = b as Element of Open_Domains_of T ;
B in { D where D is Subset of T : D is open_condensed } ;
then A3: ex D being Subset of T st
( D = B & D is open_condensed ) ;
a "/\" b = A /\ B by Def11;
hence (a "/\" b) "\/" b = Int (Cl ((A /\ B) \/ B)) by Def10
.= Int (Cl B) by XBOOLE_1:22
.= b by A3, TOPS_1:def_8 ;
::_thesis: verum
end;
A4: LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #) is join-absorbing
proof
let a, b be Element of LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #); :: according to LATTICES:def_9 ::_thesis: a "/\" (a "\/" b) = a
reconsider A = a, B = b as Element of Open_Domains_of T ;
A5: A c= A \/ (Int (Cl B)) by XBOOLE_1:7;
A in { D where D is Subset of T : D is open_condensed } ;
then ex D being Subset of T st
( D = A & D is open_condensed ) ;
then A6: A = Int (Cl A) by TOPS_1:def_8;
Int ((Cl A) \/ (Cl B)) = Int (Cl (A \/ B)) by PRE_TOPC:20;
then A7: A \/ (Int (Cl B)) c= Int (Cl (A \/ B)) by A6, TOPS_1:20;
a "\/" b = Int (Cl (A \/ B)) by Def10;
hence a "/\" (a "\/" b) = A /\ (Int (Cl (A \/ B))) by Def11
.= a by A5, A7, XBOOLE_1:1, XBOOLE_1:28 ;
::_thesis: verum
end;
A8: LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #) is meet-associative
proof
let a, b, c be Element of LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #); :: according to LATTICES:def_7 ::_thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c
reconsider A = a, B = b, C = c as Element of Open_Domains_of T ;
A9: a "/\" b = A /\ B by Def11;
b "/\" c = B /\ C by Def11;
hence a "/\" (b "/\" c) = A /\ (B /\ C) by Def11
.= (A /\ B) /\ C by XBOOLE_1:16
.= (a "/\" b) "/\" c by A9, Def11 ;
::_thesis: verum
end;
A10: LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #) is join-associative
proof
let a, b, c be Element of LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #); :: according to LATTICES:def_5 ::_thesis: a "\/" (b "\/" c) = (a "\/" b) "\/" c
reconsider A = a, B = b, C = c as Element of Open_Domains_of T ;
A in { D where D is Subset of T : D is open_condensed } ;
then A11: ex D being Subset of T st
( D = A & D is open_condensed ) ;
B in { E where E is Subset of T : E is open_condensed } ;
then A12: ex E being Subset of T st
( E = B & E is open_condensed ) ;
C in { F where F is Subset of T : F is open_condensed } ;
then A13: ex F being Subset of T st
( F = C & F is open_condensed ) ;
A14: a "\/" b = Int (Cl (A \/ B)) by Def10;
b "\/" c = Int (Cl (B \/ C)) by Def10;
hence a "\/" (b "\/" c) = Int (Cl (A \/ (Int (Cl (B \/ C))))) by Def10
.= Int (Cl ((Int (Cl (A \/ B))) \/ C)) by A11, A12, A13, Th29
.= (a "\/" b) "\/" c by A14, Def10 ;
::_thesis: verum
end;
LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #) is meet-commutative
proof
let a, b be Element of LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #); :: according to LATTICES:def_6 ::_thesis: a "/\" b = b "/\" a
reconsider A = a, B = b as Element of Open_Domains_of T ;
thus a "/\" b = B /\ A by Def11
.= b "/\" a by Def11 ; ::_thesis: verum
end;
then reconsider L = LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #) as Lattice by A1, A10, A2, A8, A4;
A15: L is upper-bounded
proof
A16: [#] T is open_condensed by Th21;
then [#] T in { D where D is Subset of T : D is open_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 Open_Domains_of T ;
thus c "\/" a = Int (Cl (C \/ A)) by Def10
.= Int (Cl C) by XBOOLE_1:12
.= c by A16, TOPS_1:def_8 ; ::_thesis: a "\/" c = c
hence a "\/" c = c ; ::_thesis: verum
end;
A17: L is distributive
proof
let a, b, c be Element of L; :: according to LATTICES:def_11 ::_thesis: a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c)
reconsider A = a, B = b, C = c as Element of Open_Domains_of T ;
A in { D where D is Subset of T : D is open_condensed } ;
then consider D being Subset of T such that
A18: D = A and
A19: D is open_condensed ;
A20: D is open by A19, TOPS_1:67;
A21: a "/\" c = A /\ C by Def11;
C in { F where F is Subset of T : F is open_condensed } ;
then consider F being Subset of T such that
A22: F = C and
F is open_condensed ;
B in { E where E is Subset of T : E is open_condensed } ;
then consider E being Subset of T such that
A23: E = B and
E is open_condensed ;
A24: a "/\" b = A /\ B by Def11;
b "\/" c = Int (Cl (B \/ C)) by Def10;
hence a "/\" (b "\/" c) = A /\ (Int (Cl (B \/ C))) by Def11
.= (Int (Cl A)) /\ (Int (Cl (B \/ C))) by A18, A19, TOPS_1:def_8
.= Int (Cl (D /\ (E \/ F))) by A18, A23, A22, A20, Th7
.= Int (Cl ((A /\ B) \/ (A /\ C))) by A18, A23, A22, XBOOLE_1:23
.= (a "/\" b) "\/" (a "/\" c) by A24, A21, Def10 ;
::_thesis: verum
end;
A25: L is complemented
proof
[#] T is open_condensed by Th21;
then [#] T in { K where K is Subset of T : K is open_condensed } ;
then reconsider c = [#] T as Element of L ;
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 Open_Domains_of T ;
B in { D where D is Subset of T : D is open_condensed } ;
then consider D being Subset of T such that
A26: D = B and
A27: D is open_condensed ;
A28: D is open by A27, TOPS_1:67;
D is condensed by A27, TOPS_1:67;
then Int (B `) is open_condensed by A26, Th16, Th25;
then Int (B `) in { K where K is Subset of T : K is open_condensed } ;
then reconsider a = Int (B `) as Element of L ;
take a ; ::_thesis: a is_a_complement_of b
A29: B ` misses B by XBOOLE_1:79;
A30: 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 Open_Domains_of T ;
thus the L_meet of L . (c,v) = ([#] T) /\ V by Def11
.= v by XBOOLE_1:28 ; ::_thesis: verum
end;
thus a "\/" b = Int (Cl (B \/ (Int (B `)))) by Def10
.= Int ([#] T) by Th9
.= c by TOPS_1:15
.= Top L by A30, LATTICE2:17 ; :: 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 open_condensed by Th20;
then {} T in { K where K is Subset of T : K is open_condensed } ;
then reconsider c = {} T as Element of L ;
A31: 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 Open_Domains_of T ;
V in { K where K is Subset of T : K is open_condensed } ;
then A32: ex D being Subset of T st
( D = V & D is open_condensed ) ;
thus the L_join of L . (c,v) = Int (Cl (({} T) \/ V)) by Def10
.= Int (Cl ((([#] T) `) \/ ((V `) `))) by XBOOLE_1:37
.= Int (Cl ((([#] T) /\ (V `)) `)) by XBOOLE_1:54
.= Int (Cl ((V `) `)) by XBOOLE_1:28
.= v by A32, TOPS_1:def_8 ; ::_thesis: verum
end;
thus a "/\" b = (Int (B `)) /\ B by Def11
.= (Int (D `)) /\ (Int D) by A26, A28, TOPS_1:23
.= Int ((B `) /\ B) by A26, TOPS_1:17
.= Int ({} T) by A29, XBOOLE_0:def_7
.= Bottom L by A31, LATTICE2:15 ; ::_thesis: b "/\" a = Bottom L
hence b "/\" a = Bottom L ; ::_thesis: verum
end;
L is lower-bounded
proof
{} T is open_condensed by Th20;
then {} T in { D where D is Subset of T : D is open_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 Open_Domains_of T ;
thus c "/\" a = C /\ A by Def11
.= c ; ::_thesis: a "/\" c = c
hence a "/\" c = c ; ::_thesis: verum
end;
hence LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #) is B_Lattice by A15, A25, A17; ::_thesis: verum
end;
definition
let T be TopSpace;
func Open_Domains_Lattice T -> B_Lattice equals :: TDLAT_1:def 12
LattStr(# (Open_Domains_of T),(Open_Domains_Union T),(Open_Domains_Meet T) #);
coherence
LattStr(# (Open_Domains_of T),(Open_Domains_Union T),(Open_Domains_Meet T) #) is B_Lattice by Th38;
end;
:: deftheorem defines Open_Domains_Lattice TDLAT_1:def_12_:_
for T being TopSpace holds Open_Domains_Lattice T = LattStr(# (Open_Domains_of T),(Open_Domains_Union T),(Open_Domains_Meet T) #);
begin
theorem Th39: :: TDLAT_1:39
for T being TopSpace holds CLD-Union T = (D-Union T) || (Closed_Domains_of T)
proof
let T be TopSpace; ::_thesis: CLD-Union T = (D-Union T) || (Closed_Domains_of T)
reconsider F = CLD-Union T as Function of [:(Closed_Domains_of T),(Closed_Domains_of T):],(Domains_of T) ;
reconsider G = (D-Union T) || (Closed_Domains_of T) as Function of [:(Closed_Domains_of T),(Closed_Domains_of T):],(Domains_of T) by FUNCT_2:32;
for A, B being Element of Closed_Domains_of T holds F . (A,B) = G . (A,B)
proof
let A, B be Element of Closed_Domains_of T; ::_thesis: F . (A,B) = G . (A,B)
thus F . (A,B) = (D-Union T) . (A,B) by Th32
.= ((D-Union T) || (Closed_Domains_of T)) . [A,B] by FUNCT_1:49
.= G . (A,B) ; ::_thesis: verum
end;
hence CLD-Union T = (D-Union T) || (Closed_Domains_of T) by BINOP_1:2; ::_thesis: verum
end;
theorem Th40: :: TDLAT_1:40
for T being TopSpace holds CLD-Meet T = (D-Meet T) || (Closed_Domains_of T)
proof
let T be TopSpace; ::_thesis: CLD-Meet T = (D-Meet T) || (Closed_Domains_of T)
reconsider F = CLD-Meet T as Function of [:(Closed_Domains_of T),(Closed_Domains_of T):],(Domains_of T) ;
reconsider G = (D-Meet T) || (Closed_Domains_of T) as Function of [:(Closed_Domains_of T),(Closed_Domains_of T):],(Domains_of T) by FUNCT_2:32;
for A, B being Element of Closed_Domains_of T holds F . (A,B) = G . (A,B)
proof
let A, B be Element of Closed_Domains_of T; ::_thesis: F . (A,B) = G . (A,B)
thus F . (A,B) = (D-Meet T) . (A,B) by Th33
.= ((D-Meet T) || (Closed_Domains_of T)) . [A,B] by FUNCT_1:49
.= G . (A,B) ; ::_thesis: verum
end;
hence CLD-Meet T = (D-Meet T) || (Closed_Domains_of T) by BINOP_1:2; ::_thesis: verum
end;
theorem :: TDLAT_1:41
for T being TopSpace holds Closed_Domains_Lattice T is SubLattice of Domains_Lattice T
proof
let T be TopSpace; ::_thesis: Closed_Domains_Lattice T is SubLattice of Domains_Lattice T
set L = Domains_Lattice T;
set CL = Closed_Domains_Lattice T;
thus the carrier of (Closed_Domains_Lattice T) c= the carrier of (Domains_Lattice T) ; :: according to NAT_LAT:def_12 ::_thesis: ( the L_join of (Closed_Domains_Lattice T) = the L_join of (Domains_Lattice T) || the carrier of (Closed_Domains_Lattice T) & the L_meet of (Closed_Domains_Lattice T) = the L_meet of (Domains_Lattice T) || the carrier of (Closed_Domains_Lattice T) )
thus the L_join of (Closed_Domains_Lattice T) = the L_join of (Domains_Lattice T) || the carrier of (Closed_Domains_Lattice T) by Th39; ::_thesis: the L_meet of (Closed_Domains_Lattice T) = the L_meet of (Domains_Lattice T) || the carrier of (Closed_Domains_Lattice T)
thus the L_meet of (Closed_Domains_Lattice T) = the L_meet of (Domains_Lattice T) || the carrier of (Closed_Domains_Lattice T) by Th40; ::_thesis: verum
end;
theorem Th42: :: TDLAT_1:42
for T being TopSpace holds OPD-Union T = (D-Union T) || (Open_Domains_of T)
proof
let T be TopSpace; ::_thesis: OPD-Union T = (D-Union T) || (Open_Domains_of T)
reconsider F = OPD-Union T as Function of [:(Open_Domains_of T),(Open_Domains_of T):],(Domains_of T) ;
reconsider G = (D-Union T) || (Open_Domains_of T) as Function of [:(Open_Domains_of T),(Open_Domains_of T):],(Domains_of T) by FUNCT_2:32;
for A, B being Element of Open_Domains_of T holds F . (A,B) = G . (A,B)
proof
let A, B be Element of Open_Domains_of T; ::_thesis: F . (A,B) = G . (A,B)
thus F . (A,B) = (D-Union T) . (A,B) by Th36
.= ((D-Union T) || (Open_Domains_of T)) . [A,B] by FUNCT_1:49
.= G . (A,B) ; ::_thesis: verum
end;
hence OPD-Union T = (D-Union T) || (Open_Domains_of T) by BINOP_1:2; ::_thesis: verum
end;
theorem Th43: :: TDLAT_1:43
for T being TopSpace holds OPD-Meet T = (D-Meet T) || (Open_Domains_of T)
proof
let T be TopSpace; ::_thesis: OPD-Meet T = (D-Meet T) || (Open_Domains_of T)
reconsider F = OPD-Meet T as Function of [:(Open_Domains_of T),(Open_Domains_of T):],(Domains_of T) ;
reconsider G = (D-Meet T) || (Open_Domains_of T) as Function of [:(Open_Domains_of T),(Open_Domains_of T):],(Domains_of T) by FUNCT_2:32;
for A, B being Element of Open_Domains_of T holds F . (A,B) = G . (A,B)
proof
let A, B be Element of Open_Domains_of T; ::_thesis: F . (A,B) = G . (A,B)
thus F . (A,B) = (D-Meet T) . (A,B) by Th37
.= ((D-Meet T) || (Open_Domains_of T)) . [A,B] by FUNCT_1:49
.= G . (A,B) ; ::_thesis: verum
end;
hence OPD-Meet T = (D-Meet T) || (Open_Domains_of T) by BINOP_1:2; ::_thesis: verum
end;
theorem :: TDLAT_1:44
for T being TopSpace holds Open_Domains_Lattice T is SubLattice of Domains_Lattice T
proof
let T be TopSpace; ::_thesis: Open_Domains_Lattice T is SubLattice of Domains_Lattice T
set L = Domains_Lattice T;
set OL = Open_Domains_Lattice T;
thus the carrier of (Open_Domains_Lattice T) c= the carrier of (Domains_Lattice T) ; :: according to NAT_LAT:def_12 ::_thesis: ( the L_join of (Open_Domains_Lattice T) = the L_join of (Domains_Lattice T) || the carrier of (Open_Domains_Lattice T) & the L_meet of (Open_Domains_Lattice T) = the L_meet of (Domains_Lattice T) || the carrier of (Open_Domains_Lattice T) )
thus the L_join of (Open_Domains_Lattice T) = the L_join of (Domains_Lattice T) || the carrier of (Open_Domains_Lattice T) by Th42; ::_thesis: the L_meet of (Open_Domains_Lattice T) = the L_meet of (Domains_Lattice T) || the carrier of (Open_Domains_Lattice T)
thus the L_meet of (Open_Domains_Lattice T) = the L_meet of (Domains_Lattice T) || the carrier of (Open_Domains_Lattice T) by Th43; ::_thesis: verum
end;