:: TDLAT_2 semantic presentation
begin
theorem Th1: :: TDLAT_2:1
for T being TopSpace
for A being Subset of T holds
( Int (Cl (Int A)) c= Int (Cl A) & Int (Cl (Int A)) c= Cl (Int A) )
proof
let T be TopSpace; ::_thesis: for A being Subset of T holds
( Int (Cl (Int A)) c= Int (Cl A) & Int (Cl (Int A)) c= Cl (Int A) )
let A be Subset of T; ::_thesis: ( Int (Cl (Int A)) c= Int (Cl A) & Int (Cl (Int A)) c= Cl (Int A) )
Cl (Int A) c= Cl A by PRE_TOPC:19, TOPS_1:16;
hence Int (Cl (Int A)) c= Int (Cl A) by TOPS_1:19; ::_thesis: Int (Cl (Int A)) c= Cl (Int A)
thus Int (Cl (Int A)) c= Cl (Int A) by TOPS_1:16; ::_thesis: verum
end;
theorem Th2: :: TDLAT_2:2
for T being TopSpace
for A being Subset of T holds
( Cl (Int A) c= Cl (Int (Cl A)) & Int (Cl A) c= Cl (Int (Cl A)) )
proof
let T be TopSpace; ::_thesis: for A being Subset of T holds
( Cl (Int A) c= Cl (Int (Cl A)) & Int (Cl A) c= Cl (Int (Cl A)) )
let A be Subset of T; ::_thesis: ( Cl (Int A) c= Cl (Int (Cl A)) & Int (Cl A) c= Cl (Int (Cl A)) )
Int A c= Int (Cl A) by PRE_TOPC:18, TOPS_1:19;
hence Cl (Int A) c= Cl (Int (Cl A)) by PRE_TOPC:19; ::_thesis: Int (Cl A) c= Cl (Int (Cl A))
thus Int (Cl A) c= Cl (Int (Cl A)) by PRE_TOPC:18; ::_thesis: verum
end;
theorem :: TDLAT_2:3
for T being TopSpace
for A, B being Subset of T st B is closed & Cl (Int (A /\ B)) = A holds
A c= B
proof
let T be TopSpace; ::_thesis: for A, B being Subset of T st B is closed & Cl (Int (A /\ B)) = A holds
A c= B
let A, B be Subset of T; ::_thesis: ( B is closed & Cl (Int (A /\ B)) = A implies A c= B )
assume A1: B is closed ; ::_thesis: ( not Cl (Int (A /\ B)) = A or A c= B )
A2: A /\ B c= B by XBOOLE_1:17;
Int (A /\ B) c= A /\ B by TOPS_1:16;
then Int (A /\ B) c= B by A2, XBOOLE_1:1;
then A3: Cl (Int (A /\ B)) c= Cl B by PRE_TOPC:19;
assume Cl (Int (A /\ B)) = A ; ::_thesis: A c= B
hence A c= B by A1, A3, PRE_TOPC:22; ::_thesis: verum
end;
theorem Th4: :: TDLAT_2:4
for T being TopSpace
for A, B being Subset of T st A is open & Int (Cl (A \/ B)) = B holds
A c= B
proof
let T be TopSpace; ::_thesis: for A, B being Subset of T st A is open & Int (Cl (A \/ B)) = B holds
A c= B
let A, B be Subset of T; ::_thesis: ( A is open & Int (Cl (A \/ B)) = B implies A c= B )
assume A1: A is open ; ::_thesis: ( not Int (Cl (A \/ B)) = B or A c= B )
A2: A c= A \/ B by XBOOLE_1:7;
A \/ B c= Cl (A \/ B) by PRE_TOPC:18;
then A c= Cl (A \/ B) by A2, XBOOLE_1:1;
then A3: Int A c= Int (Cl (A \/ B)) by TOPS_1:19;
assume Int (Cl (A \/ B)) = B ; ::_thesis: A c= B
hence A c= B by A1, A3, TOPS_1:23; ::_thesis: verum
end;
theorem Th5: :: TDLAT_2:5
for T being TopSpace
for A being Subset of T st A c= Cl (Int A) holds
A \/ (Int (Cl A)) c= Cl (Int (A \/ (Int (Cl A))))
proof
let T be TopSpace; ::_thesis: for A being Subset of T st A c= Cl (Int A) holds
A \/ (Int (Cl A)) c= Cl (Int (A \/ (Int (Cl A))))
let A be Subset of T; ::_thesis: ( A c= Cl (Int A) implies A \/ (Int (Cl A)) c= Cl (Int (A \/ (Int (Cl A)))) )
assume A1: A c= Cl (Int A) ; ::_thesis: A \/ (Int (Cl A)) c= Cl (Int (A \/ (Int (Cl A))))
A2: Int (Cl A) c= Cl (Int (Cl A)) by PRE_TOPC:18;
A3: Int A c= Int (Cl A) by PRE_TOPC:18, TOPS_1:19;
then Cl (Int A) c= Cl (Int (Cl A)) by PRE_TOPC:19;
then A c= Cl (Int (Cl A)) by A1, XBOOLE_1:1;
then A \/ (Int (Cl A)) c= (Cl (Int (Cl A))) \/ (Cl (Int (Cl A))) by A2, XBOOLE_1:13;
then A4: A \/ (Int (Cl A)) c= Cl ((Int A) \/ (Int (Cl A))) by A3, XBOOLE_1:12;
(Int A) \/ (Int (Int (Cl A))) c= Int (A \/ (Int (Cl A))) by TOPS_1:20;
then Cl ((Int A) \/ (Int (Cl A))) c= Cl (Int (A \/ (Int (Cl A)))) by PRE_TOPC:19;
hence A \/ (Int (Cl A)) c= Cl (Int (A \/ (Int (Cl A)))) by A4, XBOOLE_1:1; ::_thesis: verum
end;
theorem Th6: :: TDLAT_2:6
for T being TopSpace
for A being Subset of T st Int (Cl A) c= A holds
Int (Cl (A /\ (Cl (Int A)))) c= A /\ (Cl (Int A))
proof
let T be TopSpace; ::_thesis: for A being Subset of T st Int (Cl A) c= A holds
Int (Cl (A /\ (Cl (Int A)))) c= A /\ (Cl (Int A))
let A be Subset of T; ::_thesis: ( Int (Cl A) c= A implies Int (Cl (A /\ (Cl (Int A)))) c= A /\ (Cl (Int A)) )
assume A1: Int (Cl A) c= A ; ::_thesis: Int (Cl (A /\ (Cl (Int A)))) c= A /\ (Cl (Int A))
A2: Int (Cl (Int A)) c= Cl (Int A) by TOPS_1:16;
A3: Cl (Int A) c= Cl A by PRE_TOPC:19, TOPS_1:16;
then Int (Cl (Int A)) c= Int (Cl A) by TOPS_1:19;
then Int (Cl (Int A)) c= A by A1, XBOOLE_1:1;
then (Int (Cl (Int A))) /\ (Int (Cl (Int A))) c= A /\ (Cl (Int A)) by A2, XBOOLE_1:27;
then A4: Int ((Cl A) /\ (Cl (Int A))) c= A /\ (Cl (Int A)) by A3, XBOOLE_1:28;
Cl (A /\ (Cl (Int A))) c= (Cl A) /\ (Cl (Cl (Int A))) by PRE_TOPC:21;
then Int (Cl (A /\ (Cl (Int A)))) c= Int ((Cl A) /\ (Cl (Int A))) by TOPS_1:19;
hence Int (Cl (A /\ (Cl (Int A)))) c= A /\ (Cl (Int A)) by A4, XBOOLE_1:1; ::_thesis: verum
end;
begin
notation
let T be TopSpace;
let F be Subset-Family of T;
synonym Cl F for clf F;
end;
theorem Th7: :: TDLAT_2:7
for T being TopSpace
for F being Subset-Family of T holds Cl F = { A where A is Subset of T : ex B being Subset of T st
( A = Cl B & B in F ) }
proof
let T be TopSpace; ::_thesis: for F being Subset-Family of T holds Cl F = { A where A is Subset of T : ex B being Subset of T st
( A = Cl B & B in F ) }
let F be Subset-Family of T; ::_thesis: Cl F = { A where A is Subset of T : ex B being Subset of T st
( A = Cl B & B in F ) }
set P = { A where A is Subset of T : ex B being Subset of T st
( A = Cl B & B in F ) } ;
now__::_thesis:_for_C_being_set_st_C_in__{__A_where_A_is_Subset_of_T_:_ex_B_being_Subset_of_T_st_
(_A_=_Cl_B_&_B_in_F_)__}__holds_
C_in_bool_the_carrier_of_T
let C be set ; ::_thesis: ( C in { A where A is Subset of T : ex B being Subset of T st
( A = Cl B & B in F ) } implies C in bool the carrier of T )
assume C in { A where A is Subset of T : ex B being Subset of T st
( A = Cl B & B in F ) } ; ::_thesis: C in bool the carrier of T
then ex A being Subset of T st
( C = A & ex B being Subset of T st
( A = Cl B & B in F ) ) ;
hence C in bool the carrier of T ; ::_thesis: verum
end;
then reconsider P = { A where A is Subset of T : ex B being Subset of T st
( A = Cl B & B in F ) } as Subset-Family of T by TARSKI:def_3;
reconsider P = P as Subset-Family of T ;
for X being set holds
( X in Cl F iff X in P )
proof
let X be set ; ::_thesis: ( X in Cl F iff X in P )
A1: now__::_thesis:_(_X_in_P_implies_X_in_Cl_F_)
assume A2: X in P ; ::_thesis: X in Cl F
then reconsider C = X as Subset of T ;
ex D being Subset of T st
( D = C & ex B being Subset of T st
( D = Cl B & B in F ) ) by A2;
hence X in Cl F by PCOMPS_1:def_2; ::_thesis: verum
end;
now__::_thesis:_(_X_in_Cl_F_implies_X_in_P_)
assume A3: X in Cl F ; ::_thesis: X in P
then reconsider C = X as Subset of T ;
ex B being Subset of T st
( C = Cl B & B in F ) by A3, PCOMPS_1:def_2;
hence X in P ; ::_thesis: verum
end;
hence ( X in Cl F iff X in P ) by A1; ::_thesis: verum
end;
hence Cl F = { A where A is Subset of T : ex B being Subset of T st
( A = Cl B & B in F ) } by TARSKI:1; ::_thesis: verum
end;
theorem :: TDLAT_2:8
for T being TopSpace
for F being Subset-Family of T holds Cl F = Cl (Cl F)
proof
let T be TopSpace; ::_thesis: for F being Subset-Family of T holds Cl F = Cl (Cl F)
let F be Subset-Family of T; ::_thesis: Cl F = Cl (Cl F)
A1: Cl (Cl F) = { D where D is Subset of T : ex B being Subset of T st
( D = Cl B & B in Cl F ) } by Th7;
A2: Cl F = { A where A is Subset of T : ex B being Subset of T st
( A = Cl B & B in F ) } by Th7;
for X being set holds
( X in Cl F iff X in Cl (Cl F) )
proof
let X be set ; ::_thesis: ( X in Cl F iff X in Cl (Cl F) )
A3: now__::_thesis:_(_X_in_Cl_F_implies_X_in_Cl_(Cl_F)_)
assume A4: X in Cl F ; ::_thesis: X in Cl (Cl F)
then reconsider C = X as Subset of T ;
consider B being Subset of T such that
A5: C = Cl B and
A6: B in F by A4, PCOMPS_1:def_2;
A7: Cl B in Cl F by A6, PCOMPS_1:def_2;
C = Cl (Cl B) by A5;
hence X in Cl (Cl F) by A1, A7; ::_thesis: verum
end;
now__::_thesis:_(_X_in_Cl_(Cl_F)_implies_X_in_Cl_F_)
assume A8: X in Cl (Cl F) ; ::_thesis: X in Cl F
then reconsider C = X as Subset of T ;
ex Q being Subset of T st
( Q = C & ex B being Subset of T st
( Q = Cl B & B in Cl F ) ) by A1, A8;
then consider B being Subset of T such that
A9: C = Cl B and
A10: B in Cl F ;
ex Q being Subset of T st
( Q = B & ex R being Subset of T st
( Q = Cl R & R in F ) ) by A2, A10;
hence X in Cl F by A9, PCOMPS_1:def_2; ::_thesis: verum
end;
hence ( X in Cl F iff X in Cl (Cl F) ) by A3; ::_thesis: verum
end;
hence Cl F = Cl (Cl F) by TARSKI:1; ::_thesis: verum
end;
theorem Th9: :: TDLAT_2:9
for T being TopSpace
for F being Subset-Family of T holds
( F = {} iff Cl F = {} )
proof
let T be TopSpace; ::_thesis: for F being Subset-Family of T holds
( F = {} iff Cl F = {} )
let F be Subset-Family of T; ::_thesis: ( F = {} iff Cl F = {} )
thus ( F = {} implies Cl F = {} ) by PCOMPS_1:12; ::_thesis: ( Cl F = {} implies F = {} )
assume A1: Cl F = {} ; ::_thesis: F = {}
set B = the Element of F;
assume A2: F <> {} ; ::_thesis: contradiction
then reconsider B = the Element of F as Subset of T by TARSKI:def_3;
Cl B in Cl F by A2, PCOMPS_1:def_2;
hence contradiction by A1; ::_thesis: verum
end;
theorem :: TDLAT_2:10
for T being TopSpace
for F, G being Subset-Family of T holds Cl (F /\ G) c= (Cl F) /\ (Cl G)
proof
let T be TopSpace; ::_thesis: for F, G being Subset-Family of T holds Cl (F /\ G) c= (Cl F) /\ (Cl G)
let F, G be Subset-Family of T; ::_thesis: Cl (F /\ G) c= (Cl F) /\ (Cl G)
for X being set st X in Cl (F /\ G) holds
X in (Cl F) /\ (Cl G)
proof
let X be set ; ::_thesis: ( X in Cl (F /\ G) implies X in (Cl F) /\ (Cl G) )
assume A1: X in Cl (F /\ G) ; ::_thesis: X in (Cl F) /\ (Cl G)
then reconsider X0 = X as Subset of T ;
consider W being Subset of T such that
A2: X0 = Cl W and
A3: W in F /\ G by A1, PCOMPS_1:def_2;
W in G by A3, XBOOLE_0:def_4;
then A4: X0 in Cl G by A2, PCOMPS_1:def_2;
W in F by A3, XBOOLE_0:def_4;
then X0 in Cl F by A2, PCOMPS_1:def_2;
hence X in (Cl F) /\ (Cl G) by A4, XBOOLE_0:def_4; ::_thesis: verum
end;
hence Cl (F /\ G) c= (Cl F) /\ (Cl G) by TARSKI:def_3; ::_thesis: verum
end;
theorem :: TDLAT_2:11
for T being TopSpace
for F, G being Subset-Family of T holds (Cl F) \ (Cl G) c= Cl (F \ G)
proof
let T be TopSpace; ::_thesis: for F, G being Subset-Family of T holds (Cl F) \ (Cl G) c= Cl (F \ G)
let F, G be Subset-Family of T; ::_thesis: (Cl F) \ (Cl G) c= Cl (F \ G)
for X being set st X in (Cl F) \ (Cl G) holds
X in Cl (F \ G)
proof
let X be set ; ::_thesis: ( X in (Cl F) \ (Cl G) implies X in Cl (F \ G) )
assume A1: X in (Cl F) \ (Cl G) ; ::_thesis: X in Cl (F \ G)
then reconsider X0 = X as Subset of T ;
X in Cl F by A1, XBOOLE_0:def_5;
then consider W being Subset of T such that
A2: X0 = Cl W and
A3: W in F by PCOMPS_1:def_2;
not X in Cl G by A1, XBOOLE_0:def_5;
then not W in G by A2, PCOMPS_1:def_2;
then W in F \ G by A3, XBOOLE_0:def_5;
hence X in Cl (F \ G) by A2, PCOMPS_1:def_2; ::_thesis: verum
end;
hence (Cl F) \ (Cl G) c= Cl (F \ G) by TARSKI:def_3; ::_thesis: verum
end;
theorem :: TDLAT_2:12
for T being TopSpace
for F being Subset-Family of T
for A being Subset of T st A in F holds
( meet (Cl F) c= Cl A & Cl A c= union (Cl F) )
proof
let T be TopSpace; ::_thesis: for F being Subset-Family of T
for A being Subset of T st A in F holds
( meet (Cl F) c= Cl A & Cl A c= union (Cl F) )
let F be Subset-Family of T; ::_thesis: for A being Subset of T st A in F holds
( meet (Cl F) c= Cl A & Cl A c= union (Cl F) )
let A be Subset of T; ::_thesis: ( A in F implies ( meet (Cl F) c= Cl A & Cl A c= union (Cl F) ) )
assume A in F ; ::_thesis: ( meet (Cl F) c= Cl A & Cl A c= union (Cl F) )
then Cl A in { P where P is Subset of T : ex B being Subset of T st
( P = Cl B & B in F ) } ;
then A1: Cl A in Cl F by Th7;
hence meet (Cl F) c= Cl A by SETFAM_1:3; ::_thesis: Cl A c= union (Cl F)
thus Cl A c= union (Cl F) by A1, ZFMISC_1:74; ::_thesis: verum
end;
theorem Th13: :: TDLAT_2:13
for T being TopSpace
for F being Subset-Family of T holds meet F c= meet (Cl F)
proof
let T be TopSpace; ::_thesis: for F being Subset-Family of T holds meet F c= meet (Cl F)
let F be Subset-Family of T; ::_thesis: meet F c= meet (Cl F)
A1: for A being set st A in Cl F holds
meet F c= A
proof
let A be set ; ::_thesis: ( A in Cl F implies meet F c= A )
assume A2: A in Cl F ; ::_thesis: meet F c= A
then reconsider A0 = A as Subset of T ;
consider B being Subset of T such that
A3: A0 = Cl B and
A4: B in F by A2, PCOMPS_1:def_2;
A5: B c= A0 by A3, PRE_TOPC:18;
meet F c= B by A4, SETFAM_1:3;
hence meet F c= A by A5, XBOOLE_1:1; ::_thesis: verum
end;
now__::_thesis:_meet_F_c=_meet_(Cl_F)
percases ( Cl F = {} or Cl F <> {} ) ;
suppose Cl F = {} ; ::_thesis: meet F c= meet (Cl F)
hence meet F c= meet (Cl F) by Th9; ::_thesis: verum
end;
suppose Cl F <> {} ; ::_thesis: meet F c= meet (Cl F)
hence meet F c= meet (Cl F) by A1, SETFAM_1:5; ::_thesis: verum
end;
end;
end;
hence meet F c= meet (Cl F) ; ::_thesis: verum
end;
theorem Th14: :: TDLAT_2:14
for T being TopSpace
for F being Subset-Family of T holds Cl (meet F) c= meet (Cl F)
proof
let T be TopSpace; ::_thesis: for F being Subset-Family of T holds Cl (meet F) c= meet (Cl F)
let F be Subset-Family of T; ::_thesis: Cl (meet F) c= meet (Cl F)
A1: meet (Cl F) is closed by PCOMPS_1:11, TOPS_2:22;
Cl (meet F) c= Cl (meet (Cl F)) by Th13, PRE_TOPC:19;
hence Cl (meet F) c= meet (Cl F) by A1, PRE_TOPC:22; ::_thesis: verum
end;
theorem Th15: :: TDLAT_2:15
for T being TopSpace
for F being Subset-Family of T holds union (Cl F) c= Cl (union F)
proof
let T be TopSpace; ::_thesis: for F being Subset-Family of T holds union (Cl F) c= Cl (union F)
let F be Subset-Family of T; ::_thesis: union (Cl F) c= Cl (union F)
for A being set st A in Cl F holds
A c= Cl (union F)
proof
let A be set ; ::_thesis: ( A in Cl F implies A c= Cl (union F) )
assume A1: A in Cl F ; ::_thesis: A c= Cl (union F)
then reconsider A0 = A as Subset of T ;
ex B being Subset of T st
( A0 = Cl B & B in F ) by A1, PCOMPS_1:def_2;
hence A c= Cl (union F) by PRE_TOPC:19, ZFMISC_1:74; ::_thesis: verum
end;
hence union (Cl F) c= Cl (union F) by ZFMISC_1:76; ::_thesis: verum
end;
definition
let T be TopSpace;
let F be Subset-Family of T;
func Int F -> Subset-Family of T means :Def1: :: TDLAT_2:def 1
for A being Subset of T holds
( A in it iff ex B being Subset of T st
( A = Int B & B in F ) );
existence
ex b1 being Subset-Family of T st
for A being Subset of T holds
( A in b1 iff ex B being Subset of T st
( A = Int B & B in F ) )
proof
defpred S1[ Subset of T] means ex B being Subset of T st
( $1 = Int B & B in F );
thus ex F being Subset-Family of T st
for A being Subset of T holds
( A in F iff S1[A] ) from SUBSET_1:sch_3(); ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset-Family of T st ( for A being Subset of T holds
( A in b1 iff ex B being Subset of T st
( A = Int B & B in F ) ) ) & ( for A being Subset of T holds
( A in b2 iff ex B being Subset of T st
( A = Int B & B in F ) ) ) holds
b1 = b2
proof
let H, G be Subset-Family of T; ::_thesis: ( ( for A being Subset of T holds
( A in H iff ex B being Subset of T st
( A = Int B & B in F ) ) ) & ( for A being Subset of T holds
( A in G iff ex B being Subset of T st
( A = Int B & B in F ) ) ) implies H = G )
assume A1: for A being Subset of T holds
( A in H iff ex B being Subset of T st
( A = Int B & B in F ) ) ; ::_thesis: ( ex A being Subset of T st
( ( A in G implies ex B being Subset of T st
( A = Int B & B in F ) ) implies ( ex B being Subset of T st
( A = Int B & B in F ) & not A in G ) ) or H = G )
assume A2: for A being Subset of T holds
( A in G iff ex B being Subset of T st
( A = Int B & B in F ) ) ; ::_thesis: H = G
now__::_thesis:_for_A_being_set_st_A_in_G_holds_
A_in_H
let A be set ; ::_thesis: ( A in G implies A in H )
assume A3: A in G ; ::_thesis: A in H
then reconsider A0 = A as Subset of T ;
ex B being Subset of T st
( A0 = Int B & B in F ) by A2, A3;
hence A in H by A1; ::_thesis: verum
end;
then A4: G c= H by TARSKI:def_3;
now__::_thesis:_for_A_being_set_st_A_in_H_holds_
A_in_G
let A be set ; ::_thesis: ( A in H implies A in G )
assume A5: A in H ; ::_thesis: A in G
then reconsider A0 = A as Subset of T ;
ex B being Subset of T st
( A0 = Int B & B in F ) by A1, A5;
hence A in G by A2; ::_thesis: verum
end;
then H c= G by TARSKI:def_3;
hence H = G by A4, XBOOLE_0:def_10; ::_thesis: verum
end;
projectivity
for b1, b2 being Subset-Family of T st ( for A being Subset of T holds
( A in b1 iff ex B being Subset of T st
( A = Int B & B in b2 ) ) ) holds
for A being Subset of T holds
( A in b1 iff ex B being Subset of T st
( A = Int B & B in b1 ) )
proof
let G, F be Subset-Family of T; ::_thesis: ( ( for A being Subset of T holds
( A in G iff ex B being Subset of T st
( A = Int B & B in F ) ) ) implies for A being Subset of T holds
( A in G iff ex B being Subset of T st
( A = Int B & B in G ) ) )
assume A6: for A being Subset of T holds
( A in G iff ex B being Subset of T st
( A = Int B & B in F ) ) ; ::_thesis: for A being Subset of T holds
( A in G iff ex B being Subset of T st
( A = Int B & B in G ) )
let A be Subset of T; ::_thesis: ( A in G iff ex B being Subset of T st
( A = Int B & B in G ) )
thus ( A in G implies ex B being Subset of T st
( A = Int B & B in G ) ) ::_thesis: ( ex B being Subset of T st
( A = Int B & B in G ) implies A in G )
proof
assume A in G ; ::_thesis: ex B being Subset of T st
( A = Int B & B in G )
then consider B being Subset of T such that
A7: A = Int B and
A8: B in F by A6;
take C = Int B; ::_thesis: ( A = Int C & C in G )
thus A = Int C by A7; ::_thesis: C in G
thus C in G by A8, A6; ::_thesis: verum
end;
given B being Subset of T such that A9: A = Int B and
A10: B in G ; ::_thesis: A in G
consider C being Subset of T such that
A11: B = Int C and
C in F by A10, A6;
A = B by A9, A11;
hence A in G by A10; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines Int TDLAT_2:def_1_:_
for T being TopSpace
for F, b3 being Subset-Family of T holds
( b3 = Int F iff for A being Subset of T holds
( A in b3 iff ex B being Subset of T st
( A = Int B & B in F ) ) );
theorem Th16: :: TDLAT_2:16
for T being TopSpace
for F being Subset-Family of T holds Int F = { A where A is Subset of T : ex B being Subset of T st
( A = Int B & B in F ) }
proof
let T be TopSpace; ::_thesis: for F being Subset-Family of T holds Int F = { A where A is Subset of T : ex B being Subset of T st
( A = Int B & B in F ) }
let F be Subset-Family of T; ::_thesis: Int F = { A where A is Subset of T : ex B being Subset of T st
( A = Int B & B in F ) }
set P = { A where A is Subset of T : ex B being Subset of T st
( A = Int B & B in F ) } ;
now__::_thesis:_for_C_being_set_st_C_in__{__A_where_A_is_Subset_of_T_:_ex_B_being_Subset_of_T_st_
(_A_=_Int_B_&_B_in_F_)__}__holds_
C_in_bool_the_carrier_of_T
let C be set ; ::_thesis: ( C in { A where A is Subset of T : ex B being Subset of T st
( A = Int B & B in F ) } implies C in bool the carrier of T )
assume C in { A where A is Subset of T : ex B being Subset of T st
( A = Int B & B in F ) } ; ::_thesis: C in bool the carrier of T
then ex A being Subset of T st
( C = A & ex B being Subset of T st
( A = Int B & B in F ) ) ;
hence C in bool the carrier of T ; ::_thesis: verum
end;
then reconsider P = { A where A is Subset of T : ex B being Subset of T st
( A = Int B & B in F ) } as Subset-Family of T by TARSKI:def_3;
reconsider P = P as Subset-Family of T ;
for X being set holds
( X in Int F iff X in P )
proof
let X be set ; ::_thesis: ( X in Int F iff X in P )
A1: now__::_thesis:_(_X_in_P_implies_X_in_Int_F_)
assume A2: X in P ; ::_thesis: X in Int F
then reconsider C = X as Subset of T ;
ex D being Subset of T st
( D = C & ex B being Subset of T st
( D = Int B & B in F ) ) by A2;
hence X in Int F by Def1; ::_thesis: verum
end;
now__::_thesis:_(_X_in_Int_F_implies_X_in_P_)
assume A3: X in Int F ; ::_thesis: X in P
then reconsider C = X as Subset of T ;
ex B being Subset of T st
( C = Int B & B in F ) by A3, Def1;
hence X in P ; ::_thesis: verum
end;
hence ( X in Int F iff X in P ) by A1; ::_thesis: verum
end;
hence Int F = { A where A is Subset of T : ex B being Subset of T st
( A = Int B & B in F ) } by TARSKI:1; ::_thesis: verum
end;
theorem :: TDLAT_2:17
canceled;
theorem Th18: :: TDLAT_2:18
for T being TopSpace
for F being Subset-Family of T holds Int F is open
proof
let T be TopSpace; ::_thesis: for F being Subset-Family of T holds Int F is open
let F be Subset-Family of T; ::_thesis: Int F is open
now__::_thesis:_for_A_being_Subset_of_T_st_A_in_Int_F_holds_
A_is_open
let A be Subset of T; ::_thesis: ( A in Int F implies A is open )
assume A in Int F ; ::_thesis: A is open
then ex B being Subset of T st
( A = Int B & B in F ) by Def1;
hence A is open ; ::_thesis: verum
end;
hence Int F is open by TOPS_2:def_1; ::_thesis: verum
end;
theorem Th19: :: TDLAT_2:19
for T being TopSpace
for F being Subset-Family of T holds
( F = {} iff Int F = {} )
proof
let T be TopSpace; ::_thesis: for F being Subset-Family of T holds
( F = {} iff Int F = {} )
let F be Subset-Family of T; ::_thesis: ( F = {} iff Int F = {} )
thus ( F = {} implies Int F = {} ) ::_thesis: ( Int F = {} implies F = {} )
proof
set A = the Element of Int F;
assume A1: F = {} ; ::_thesis: Int F = {}
assume A2: not Int F = {} ; ::_thesis: contradiction
then reconsider A = the Element of Int F as Subset of T by TARSKI:def_3;
ex V being Subset of T st
( A = Int V & V in F ) by A2, Def1;
hence contradiction by A1; ::_thesis: verum
end;
thus ( Int F = {} implies F = {} ) ::_thesis: verum
proof
set B = the Element of F;
assume A3: Int F = {} ; ::_thesis: F = {}
assume A4: not F = {} ; ::_thesis: contradiction
then reconsider B = the Element of F as Subset of T by TARSKI:def_3;
reconsider A = Int B as set ;
ex A being set st A in Int F
proof
take A ; ::_thesis: A in Int F
thus A in Int F by A4, Def1; ::_thesis: verum
end;
hence contradiction by A3; ::_thesis: verum
end;
end;
theorem Th20: :: TDLAT_2:20
for T being TopSpace
for A being Subset of T
for F being Subset-Family of T st F = {A} holds
Int F = {(Int A)}
proof
let T be TopSpace; ::_thesis: for A being Subset of T
for F being Subset-Family of T st F = {A} holds
Int F = {(Int A)}
let A be Subset of T; ::_thesis: for F being Subset-Family of T st F = {A} holds
Int F = {(Int A)}
let F be Subset-Family of T; ::_thesis: ( F = {A} implies Int F = {(Int A)} )
reconsider C = Int F as set ;
assume A1: F = {A} ; ::_thesis: Int F = {(Int A)}
for B being set holds
( B in C iff B = Int A )
proof
let B be set ; ::_thesis: ( B in C iff B = Int A )
A2: now__::_thesis:_(_B_=_Int_A_implies_B_in_C_)
assume A3: B = Int A ; ::_thesis: B in C
ex M being Subset of T st
( B = Int M & M in F )
proof
take A ; ::_thesis: ( B = Int A & A in F )
thus ( B = Int A & A in F ) by A1, A3, TARSKI:def_1; ::_thesis: verum
end;
hence B in C by Def1; ::_thesis: verum
end;
now__::_thesis:_(_B_in_C_implies_B_=_Int_A_)
assume A4: B in C ; ::_thesis: B = Int A
then reconsider B0 = B as Subset of T ;
ex M being Subset of T st
( B0 = Int M & M in F ) by A4, Def1;
hence B = Int A by A1, TARSKI:def_1; ::_thesis: verum
end;
hence ( B in C iff B = Int A ) by A2; ::_thesis: verum
end;
hence Int F = {(Int A)} by TARSKI:def_1; ::_thesis: verum
end;
theorem :: TDLAT_2:21
for T being TopSpace
for F, G being Subset-Family of T st F c= G holds
Int F c= Int G
proof
let T be TopSpace; ::_thesis: for F, G being Subset-Family of T st F c= G holds
Int F c= Int G
let F, G be Subset-Family of T; ::_thesis: ( F c= G implies Int F c= Int G )
reconsider F0 = Int F, G0 = Int G as set ;
assume A1: F c= G ; ::_thesis: Int F c= Int G
now__::_thesis:_for_X_being_set_st_X_in_F0_holds_
X_in_G0
let X be set ; ::_thesis: ( X in F0 implies X in G0 )
assume A2: X in F0 ; ::_thesis: X in G0
then reconsider X0 = X as Subset of T ;
ex V being Subset of T st
( X0 = Int V & V in F ) by A2, Def1;
hence X in G0 by A1, Def1; ::_thesis: verum
end;
hence Int F c= Int G by TARSKI:def_3; ::_thesis: verum
end;
theorem Th22: :: TDLAT_2:22
for T being TopSpace
for F, G being Subset-Family of T holds Int (F \/ G) = (Int F) \/ (Int G)
proof
let T be TopSpace; ::_thesis: for F, G being Subset-Family of T holds Int (F \/ G) = (Int F) \/ (Int G)
let F, G be Subset-Family of T; ::_thesis: Int (F \/ G) = (Int F) \/ (Int G)
for X being set holds
( X in Int (F \/ G) iff X in (Int F) \/ (Int G) )
proof
let X be set ; ::_thesis: ( X in Int (F \/ G) iff X in (Int F) \/ (Int G) )
A1: now__::_thesis:_(_X_in_(Int_F)_\/_(Int_G)_implies_X_in_Int_(F_\/_G)_)
assume A2: X in (Int F) \/ (Int G) ; ::_thesis: X in Int (F \/ G)
now__::_thesis:_X_in_Int_(F_\/_G)
percases ( X in Int F or X in Int G ) by A2, XBOOLE_0:def_3;
supposeA3: X in Int F ; ::_thesis: X in Int (F \/ G)
then reconsider X0 = X as Subset of T ;
ex W being Subset of T st
( X0 = Int W & W in F \/ G )
proof
consider Z being Subset of T such that
A4: X0 = Int Z and
A5: Z in F by A3, Def1;
take Z ; ::_thesis: ( X0 = Int Z & Z in F \/ G )
thus ( X0 = Int Z & Z in F \/ G ) by A4, A5, XBOOLE_0:def_3; ::_thesis: verum
end;
hence X in Int (F \/ G) by Def1; ::_thesis: verum
end;
supposeA6: X in Int G ; ::_thesis: X in Int (F \/ G)
then reconsider X0 = X as Subset of T ;
ex W being Subset of T st
( X0 = Int W & W in F \/ G )
proof
consider Z being Subset of T such that
A7: X0 = Int Z and
A8: Z in G by A6, Def1;
take Z ; ::_thesis: ( X0 = Int Z & Z in F \/ G )
thus ( X0 = Int Z & Z in F \/ G ) by A7, A8, XBOOLE_0:def_3; ::_thesis: verum
end;
hence X in Int (F \/ G) by Def1; ::_thesis: verum
end;
end;
end;
hence X in Int (F \/ G) ; ::_thesis: verum
end;
now__::_thesis:_(_X_in_Int_(F_\/_G)_implies_X_in_(Int_F)_\/_(Int_G)_)
assume A9: X in Int (F \/ G) ; ::_thesis: X in (Int F) \/ (Int G)
then reconsider X0 = X as Subset of T ;
consider W being Subset of T such that
A10: X0 = Int W and
A11: W in F \/ G by A9, Def1;
now__::_thesis:_X0_in_(Int_F)_\/_(Int_G)
percases ( W in F or W in G ) by A11, XBOOLE_0:def_3;
suppose W in F ; ::_thesis: X0 in (Int F) \/ (Int G)
then X0 in Int F by A10, Def1;
hence X0 in (Int F) \/ (Int G) by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose W in G ; ::_thesis: X0 in (Int F) \/ (Int G)
then X0 in Int G by A10, Def1;
hence X0 in (Int F) \/ (Int G) by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
hence X in (Int F) \/ (Int G) ; ::_thesis: verum
end;
hence ( X in Int (F \/ G) iff X in (Int F) \/ (Int G) ) by A1; ::_thesis: verum
end;
hence Int (F \/ G) = (Int F) \/ (Int G) by TARSKI:1; ::_thesis: verum
end;
theorem :: TDLAT_2:23
for T being TopSpace
for F, G being Subset-Family of T holds Int (F /\ G) c= (Int F) /\ (Int G)
proof
let T be TopSpace; ::_thesis: for F, G being Subset-Family of T holds Int (F /\ G) c= (Int F) /\ (Int G)
let F, G be Subset-Family of T; ::_thesis: Int (F /\ G) c= (Int F) /\ (Int G)
for X being set st X in Int (F /\ G) holds
X in (Int F) /\ (Int G)
proof
let X be set ; ::_thesis: ( X in Int (F /\ G) implies X in (Int F) /\ (Int G) )
assume A1: X in Int (F /\ G) ; ::_thesis: X in (Int F) /\ (Int G)
then reconsider X0 = X as Subset of T ;
consider W being Subset of T such that
A2: X0 = Int W and
A3: W in F /\ G by A1, Def1;
W in G by A3, XBOOLE_0:def_4;
then A4: X0 in Int G by A2, Def1;
W in F by A3, XBOOLE_0:def_4;
then X0 in Int F by A2, Def1;
hence X in (Int F) /\ (Int G) by A4, XBOOLE_0:def_4; ::_thesis: verum
end;
hence Int (F /\ G) c= (Int F) /\ (Int G) by TARSKI:def_3; ::_thesis: verum
end;
theorem :: TDLAT_2:24
for T being TopSpace
for F, G being Subset-Family of T holds (Int F) \ (Int G) c= Int (F \ G)
proof
let T be TopSpace; ::_thesis: for F, G being Subset-Family of T holds (Int F) \ (Int G) c= Int (F \ G)
let F, G be Subset-Family of T; ::_thesis: (Int F) \ (Int G) c= Int (F \ G)
for X being set st X in (Int F) \ (Int G) holds
X in Int (F \ G)
proof
let X be set ; ::_thesis: ( X in (Int F) \ (Int G) implies X in Int (F \ G) )
assume A1: X in (Int F) \ (Int G) ; ::_thesis: X in Int (F \ G)
then reconsider X0 = X as Subset of T ;
X in Int F by A1, XBOOLE_0:def_5;
then consider W being Subset of T such that
A2: X0 = Int W and
A3: W in F by Def1;
not X in Int G by A1, XBOOLE_0:def_5;
then not W in G by A2, Def1;
then W in F \ G by A3, XBOOLE_0:def_5;
hence X in Int (F \ G) by A2, Def1; ::_thesis: verum
end;
hence (Int F) \ (Int G) c= Int (F \ G) by TARSKI:def_3; ::_thesis: verum
end;
theorem :: TDLAT_2:25
for T being TopSpace
for F being Subset-Family of T
for A being Subset of T st A in F holds
( Int A c= union (Int F) & meet (Int F) c= Int A )
proof
let T be TopSpace; ::_thesis: for F being Subset-Family of T
for A being Subset of T st A in F holds
( Int A c= union (Int F) & meet (Int F) c= Int A )
let F be Subset-Family of T; ::_thesis: for A being Subset of T st A in F holds
( Int A c= union (Int F) & meet (Int F) c= Int A )
let A be Subset of T; ::_thesis: ( A in F implies ( Int A c= union (Int F) & meet (Int F) c= Int A ) )
assume A in F ; ::_thesis: ( Int A c= union (Int F) & meet (Int F) c= Int A )
then Int A in { P where P is Subset of T : ex B being Subset of T st
( P = Int B & B in F ) } ;
then A1: Int A in Int F by Th16;
hence Int A c= union (Int F) by ZFMISC_1:74; ::_thesis: meet (Int F) c= Int A
thus meet (Int F) c= Int A by A1, SETFAM_1:3; ::_thesis: verum
end;
theorem Th26: :: TDLAT_2:26
for T being TopSpace
for F being Subset-Family of T holds union (Int F) c= union F
proof
let T be TopSpace; ::_thesis: for F being Subset-Family of T holds union (Int F) c= union F
let F be Subset-Family of T; ::_thesis: union (Int F) c= union F
now__::_thesis:_for_x_being_set_st_x_in_union_(Int_F)_holds_
x_in_union_F
let x be set ; ::_thesis: ( x in union (Int F) implies x in union F )
assume x in union (Int F) ; ::_thesis: x in union F
then consider A being set such that
A1: x in A and
A2: A in Int F by TARSKI:def_4;
reconsider A = A as Subset of T by A2;
consider B being Subset of T such that
A3: A = Int B and
A4: B in F by A2, Def1;
ex B being set st
( x in B & B in F )
proof
take B ; ::_thesis: ( x in B & B in F )
Int B c= B by TOPS_1:16;
hence ( x in B & B in F ) by A1, A3, A4; ::_thesis: verum
end;
hence x in union F by TARSKI:def_4; ::_thesis: verum
end;
hence union (Int F) c= union F by TARSKI:def_3; ::_thesis: verum
end;
theorem :: TDLAT_2:27
for T being TopSpace
for F being Subset-Family of T holds meet (Int F) c= meet F
proof
let T be TopSpace; ::_thesis: for F being Subset-Family of T holds meet (Int F) c= meet F
let F be Subset-Family of T; ::_thesis: meet (Int F) c= meet F
A1: for A being set st A in F holds
meet (Int F) c= A
proof
let A be set ; ::_thesis: ( A in F implies meet (Int F) c= A )
assume A2: A in F ; ::_thesis: meet (Int F) c= A
then reconsider A0 = A as Subset of T ;
set C = Int A0;
Int A0 in { P where P is Subset of T : ex Q being Subset of T st
( P = Int Q & Q in F ) } by A2;
then Int A0 in Int F by Th16;
then A3: meet (Int F) c= Int A0 by SETFAM_1:3;
Int A0 c= A0 by TOPS_1:16;
hence meet (Int F) c= A by A3, XBOOLE_1:1; ::_thesis: verum
end;
now__::_thesis:_meet_(Int_F)_c=_meet_F
percases ( F = {} or F <> {} ) ;
suppose F = {} ; ::_thesis: meet (Int F) c= meet F
hence meet (Int F) c= meet F by Th19; ::_thesis: verum
end;
suppose F <> {} ; ::_thesis: meet (Int F) c= meet F
hence meet (Int F) c= meet F by A1, SETFAM_1:5; ::_thesis: verum
end;
end;
end;
hence meet (Int F) c= meet F ; ::_thesis: verum
end;
theorem Th28: :: TDLAT_2:28
for T being TopSpace
for F being Subset-Family of T holds union (Int F) c= Int (union F)
proof
let T be TopSpace; ::_thesis: for F being Subset-Family of T holds union (Int F) c= Int (union F)
let F be Subset-Family of T; ::_thesis: union (Int F) c= Int (union F)
A1: Int (union (Int F)) c= Int (union F) by Th26, TOPS_1:19;
union (Int F) is open by Th18, TOPS_2:19;
hence union (Int F) c= Int (union F) by A1, TOPS_1:23; ::_thesis: verum
end;
theorem Th29: :: TDLAT_2:29
for T being TopSpace
for F being Subset-Family of T holds Int (meet F) c= meet (Int F)
proof
let T be TopSpace; ::_thesis: for F being Subset-Family of T holds Int (meet F) c= meet (Int F)
let F be Subset-Family of T; ::_thesis: Int (meet F) c= meet (Int F)
A1: for A being set st A in Int F holds
Int (meet F) c= A
proof
let A be set ; ::_thesis: ( A in Int F implies Int (meet F) c= A )
assume A2: A in Int F ; ::_thesis: Int (meet F) c= A
then reconsider A0 = A as Subset of T ;
A0 in { B where B is Subset of T : ex C being Subset of T st
( B = Int C & C in F ) } by A2, Th16;
then ex P being Subset of T st
( P = A0 & ex C being Subset of T st
( P = Int C & C in F ) ) ;
hence Int (meet F) c= A by SETFAM_1:3, TOPS_1:19; ::_thesis: verum
end;
now__::_thesis:_Int_(meet_F)_c=_meet_(Int_F)
percases ( Int F = {} or Int F <> {} ) ;
supposeA3: Int F = {} ; ::_thesis: Int (meet F) c= meet (Int F)
then meet F = {} T by Th19, SETFAM_1:1;
hence Int (meet F) c= meet (Int F) by A3, SETFAM_1:1; ::_thesis: verum
end;
suppose Int F <> {} ; ::_thesis: Int (meet F) c= meet (Int F)
hence Int (meet F) c= meet (Int F) by A1, SETFAM_1:5; ::_thesis: verum
end;
end;
end;
hence Int (meet F) c= meet (Int F) ; ::_thesis: verum
end;
theorem :: TDLAT_2:30
for T being TopSpace
for F being Subset-Family of T st F is finite holds
Int (meet F) = meet (Int F)
proof
let T be TopSpace; ::_thesis: for F being Subset-Family of T st F is finite holds
Int (meet F) = meet (Int F)
let F be Subset-Family of T; ::_thesis: ( F is finite implies Int (meet F) = meet (Int F) )
assume A1: F is finite ; ::_thesis: Int (meet F) = meet (Int F)
A2: meet (Int F) c= Int (meet F)
proof
consider p being FinSequence such that
A3: rng p = F by A1, FINSEQ_1:52;
consider n being Nat such that
A4: dom p = Seg n by FINSEQ_1:def_2;
defpred S1[ Nat] means for G being Subset-Family of T st G = p .: (Seg $1) & $1 <= n & 1 <= n holds
meet (Int G) c= Int (meet G);
A5: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A6: for G being Subset-Family of T st G = p .: (Seg k) & k <= n & 1 <= n holds
meet (Int G) c= Int (meet G) ; ::_thesis: S1[k + 1]
let G be Subset-Family of T; ::_thesis: ( G = p .: (Seg (k + 1)) & k + 1 <= n & 1 <= n implies meet (Int G) c= Int (meet G) )
assume A7: G = p .: (Seg (k + 1)) ; ::_thesis: ( not k + 1 <= n or not 1 <= n or meet (Int G) c= Int (meet G) )
assume that
A8: k + 1 <= n and
A9: 1 <= n ; ::_thesis: meet (Int G) c= Int (meet G)
A10: now__::_thesis:_(_0_<_k_implies_meet_(Int_G)_c=_Int_(meet_G)_)
reconsider G2 = Im (p,(k + 1)) as Subset-Family of T by A3, RELAT_1:111, TOPS_2:2;
reconsider G1 = p .: (Seg k) as Subset-Family of T by A3, RELAT_1:111, TOPS_2:2;
A11: 0 + 1 = 1 ;
0 <= k by NAT_1:2;
then 1 <= k + 1 by A11, XREAL_1:7;
then A12: k + 1 in dom p by A4, A8, FINSEQ_1:1;
then A13: G2 = {(p . (k + 1))} by FUNCT_1:59;
then meet G2 = p . (k + 1) by SETFAM_1:10;
then reconsider G3 = p . (k + 1) as Subset of T ;
A14: meet (Int G2) = meet {(Int G3)} by A13, Th20
.= Int G3 by SETFAM_1:10
.= Int (meet G2) by A13, SETFAM_1:10 ;
k + 1 <= n + 1 by A8, NAT_1:12;
then k <= n by XREAL_1:6;
then A15: meet (Int G1) c= Int (meet G1) by A6, A9;
assume 0 < k ; ::_thesis: meet (Int G) c= Int (meet G)
then A16: 0 + 1 <= k by NAT_1:13;
then A17: k in Seg k by FINSEQ_1:1;
k <= n by A8, NAT_1:13;
then k in dom p by A4, A16, FINSEQ_1:1;
then A18: p . k in G1 by A17, FUNCT_1:def_6;
k + 1 in {(k + 1)} by TARSKI:def_1;
then A19: p . (k + 1) in G2 by A12, FUNCT_1:def_6;
then A20: Int G2 <> {} by Th19;
A21: p .: (Seg (k + 1)) = p .: ((Seg k) \/ {(k + 1)}) by FINSEQ_1:9
.= (p .: (Seg k)) \/ (p .: {(k + 1)}) by RELAT_1:120 ;
then Int (meet G) = Int ((meet G1) /\ (meet G2)) by A7, A18, A19, SETFAM_1:9
.= (Int (meet G1)) /\ (Int (meet G2)) by TOPS_1:17 ;
then A22: (meet (Int G1)) /\ (meet (Int G2)) c= Int (meet G) by A14, A15, XBOOLE_1:27;
Int G1 <> {} by A18, Th19;
then meet ((Int G1) \/ (Int G2)) c= Int (meet G) by A20, A22, SETFAM_1:9;
hence meet (Int G) c= Int (meet G) by A7, A21, Th22; ::_thesis: verum
end;
now__::_thesis:_(_k_=_0_implies_meet_(Int_G)_c=_Int_(meet_G)_)
assume A23: k = 0 ; ::_thesis: meet (Int G) c= Int (meet G)
then 1 in dom p by A4, A8, FINSEQ_1:1;
then A24: Im (p,1) = {(p . 1)} by FUNCT_1:59;
then union G = p . 1 by A7, A23, FINSEQ_1:2, ZFMISC_1:25;
then reconsider G1 = p . 1 as Subset of T ;
Int (meet G) = Int G1 by A7, A23, A24, FINSEQ_1:2, SETFAM_1:10
.= meet {(Int G1)} by SETFAM_1:10
.= meet (Int G) by A7, A23, A24, Th20, FINSEQ_1:2 ;
hence meet (Int G) c= Int (meet G) ; ::_thesis: verum
end;
hence meet (Int G) c= Int (meet G) by A10, NAT_1:3; ::_thesis: verum
end;
A25: S1[ 0 ] by Th19, SETFAM_1:1;
A27: for k being Nat holds S1[k] from NAT_1:sch_2(A25, A5);
A28: now__::_thesis:_(_1_<=_n_implies_meet_(Int_F)_c=_Int_(meet_F)_)
assume A29: 1 <= n ; ::_thesis: meet (Int F) c= Int (meet F)
F = p .: (Seg n) by A3, A4, RELAT_1:113;
hence meet (Int F) c= Int (meet F) by A27, A29; ::_thesis: verum
end;
A30: now__::_thesis:_(_n_<>_0_implies_1_<=_n_)
assume n <> 0 ; ::_thesis: 1 <= n
then A31: 0 < n by NAT_1:3;
1 = 0 + 1 ;
hence 1 <= n by A31, NAT_1:13; ::_thesis: verum
end;
now__::_thesis:_(_n_=_0_implies_meet_(Int_F)_c=_Int_(meet_F)_)
assume n = 0 ; ::_thesis: meet (Int F) c= Int (meet F)
then Seg n = {} ;
then F = p .: {} by A3, A4, RELAT_1:113;
then F = {} ;
hence meet (Int F) c= Int (meet F) by Th19, SETFAM_1:1; ::_thesis: verum
end;
hence meet (Int F) c= Int (meet F) by A28, A30; ::_thesis: verum
end;
Int (meet F) c= meet (Int F) by Th29;
hence Int (meet F) = meet (Int F) by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th31: :: TDLAT_2:31
for T being non empty TopSpace
for F being Subset-Family of T holds Cl (Int F) = { A where A is Subset of T : ex B being Subset of T st
( A = Cl (Int B) & B in F ) }
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds Cl (Int F) = { A where A is Subset of T : ex B being Subset of T st
( A = Cl (Int B) & B in F ) }
let F be Subset-Family of T; ::_thesis: Cl (Int F) = { A where A is Subset of T : ex B being Subset of T st
( A = Cl (Int B) & B in F ) }
set P = { A where A is Subset of T : ex B being Subset of T st
( A = Cl (Int B) & B in F ) } ;
now__::_thesis:_for_C_being_set_st_C_in__{__A_where_A_is_Subset_of_T_:_ex_B_being_Subset_of_T_st_
(_A_=_Cl_(Int_B)_&_B_in_F_)__}__holds_
C_in_bool_the_carrier_of_T
let C be set ; ::_thesis: ( C in { A where A is Subset of T : ex B being Subset of T st
( A = Cl (Int B) & B in F ) } implies C in bool the carrier of T )
assume C in { A where A is Subset of T : ex B being Subset of T st
( A = Cl (Int B) & B in F ) } ; ::_thesis: C in bool the carrier of T
then ex A being Subset of T st
( C = A & ex B being Subset of T st
( A = Cl (Int B) & B in F ) ) ;
hence C in bool the carrier of T ; ::_thesis: verum
end;
then reconsider P = { A where A is Subset of T : ex B being Subset of T st
( A = Cl (Int B) & B in F ) } as Subset-Family of T by TARSKI:def_3;
reconsider P = P as Subset-Family of T ;
for X being set holds
( X in Cl (Int F) iff X in P )
proof
let X be set ; ::_thesis: ( X in Cl (Int F) iff X in P )
A1: now__::_thesis:_(_X_in_P_implies_X_in_Cl_(Int_F)_)
assume A2: X in P ; ::_thesis: X in Cl (Int F)
then reconsider C = X as Subset of T ;
ex D being Subset of T st
( D = C & ex B being Subset of T st
( D = Cl (Int B) & B in F ) ) by A2;
then consider B being Subset of T such that
A3: C = Cl (Int B) and
A4: B in F ;
Int B in Int F by A4, Def1;
hence X in Cl (Int F) by A3, PCOMPS_1:def_2; ::_thesis: verum
end;
now__::_thesis:_(_X_in_Cl_(Int_F)_implies_X_in_P_)
assume A5: X in Cl (Int F) ; ::_thesis: X in P
then reconsider C = X as Subset of T ;
consider B being Subset of T such that
A6: C = Cl B and
A7: B in Int F by A5, PCOMPS_1:def_2;
ex D being Subset of T st
( B = Int D & D in F ) by A7, Def1;
hence X in P by A6; ::_thesis: verum
end;
hence ( X in Cl (Int F) iff X in P ) by A1; ::_thesis: verum
end;
hence Cl (Int F) = { A where A is Subset of T : ex B being Subset of T st
( A = Cl (Int B) & B in F ) } by TARSKI:1; ::_thesis: verum
end;
theorem Th32: :: TDLAT_2:32
for T being non empty TopSpace
for F being Subset-Family of T holds Int (Cl F) = { A where A is Subset of T : ex B being Subset of T st
( A = Int (Cl B) & B in F ) }
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds Int (Cl F) = { A where A is Subset of T : ex B being Subset of T st
( A = Int (Cl B) & B in F ) }
let F be Subset-Family of T; ::_thesis: Int (Cl F) = { A where A is Subset of T : ex B being Subset of T st
( A = Int (Cl B) & B in F ) }
set P = { A where A is Subset of T : ex B being Subset of T st
( A = Int (Cl B) & B in F ) } ;
now__::_thesis:_for_C_being_set_st_C_in__{__A_where_A_is_Subset_of_T_:_ex_B_being_Subset_of_T_st_
(_A_=_Int_(Cl_B)_&_B_in_F_)__}__holds_
C_in_bool_the_carrier_of_T
let C be set ; ::_thesis: ( C in { A where A is Subset of T : ex B being Subset of T st
( A = Int (Cl B) & B in F ) } implies C in bool the carrier of T )
assume C in { A where A is Subset of T : ex B being Subset of T st
( A = Int (Cl B) & B in F ) } ; ::_thesis: C in bool the carrier of T
then ex A being Subset of T st
( C = A & ex B being Subset of T st
( A = Int (Cl B) & B in F ) ) ;
hence C in bool the carrier of T ; ::_thesis: verum
end;
then reconsider P = { A where A is Subset of T : ex B being Subset of T st
( A = Int (Cl B) & B in F ) } as Subset-Family of T by TARSKI:def_3;
reconsider P = P as Subset-Family of T ;
for X being set holds
( X in Int (Cl F) iff X in P )
proof
let X be set ; ::_thesis: ( X in Int (Cl F) iff X in P )
A1: now__::_thesis:_(_X_in_P_implies_X_in_Int_(Cl_F)_)
assume A2: X in P ; ::_thesis: X in Int (Cl F)
then reconsider C = X as Subset of T ;
ex D being Subset of T st
( D = C & ex B being Subset of T st
( D = Int (Cl B) & B in F ) ) by A2;
then consider B being Subset of T such that
A3: C = Int (Cl B) and
A4: B in F ;
Cl B in Cl F by A4, PCOMPS_1:def_2;
hence X in Int (Cl F) by A3, Def1; ::_thesis: verum
end;
now__::_thesis:_(_X_in_Int_(Cl_F)_implies_X_in_P_)
assume A5: X in Int (Cl F) ; ::_thesis: X in P
then reconsider C = X as Subset of T ;
consider B being Subset of T such that
A6: C = Int B and
A7: B in Cl F by A5, Def1;
ex D being Subset of T st
( B = Cl D & D in F ) by A7, PCOMPS_1:def_2;
hence X in P by A6; ::_thesis: verum
end;
hence ( X in Int (Cl F) iff X in P ) by A1; ::_thesis: verum
end;
hence Int (Cl F) = { A where A is Subset of T : ex B being Subset of T st
( A = Int (Cl B) & B in F ) } by TARSKI:1; ::_thesis: verum
end;
theorem Th33: :: TDLAT_2:33
for T being non empty TopSpace
for F being Subset-Family of T holds Cl (Int (Cl F)) = { A where A is Subset of T : ex B being Subset of T st
( A = Cl (Int (Cl B)) & B in F ) }
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds Cl (Int (Cl F)) = { A where A is Subset of T : ex B being Subset of T st
( A = Cl (Int (Cl B)) & B in F ) }
let F be Subset-Family of T; ::_thesis: Cl (Int (Cl F)) = { A where A is Subset of T : ex B being Subset of T st
( A = Cl (Int (Cl B)) & B in F ) }
set P = { A where A is Subset of T : ex B being Subset of T st
( A = Cl (Int (Cl B)) & B in F ) } ;
now__::_thesis:_for_C_being_set_st_C_in__{__A_where_A_is_Subset_of_T_:_ex_B_being_Subset_of_T_st_
(_A_=_Cl_(Int_(Cl_B))_&_B_in_F_)__}__holds_
C_in_bool_the_carrier_of_T
let C be set ; ::_thesis: ( C in { A where A is Subset of T : ex B being Subset of T st
( A = Cl (Int (Cl B)) & B in F ) } implies C in bool the carrier of T )
assume C in { A where A is Subset of T : ex B being Subset of T st
( A = Cl (Int (Cl B)) & B in F ) } ; ::_thesis: C in bool the carrier of T
then ex A being Subset of T st
( C = A & ex B being Subset of T st
( A = Cl (Int (Cl B)) & B in F ) ) ;
hence C in bool the carrier of T ; ::_thesis: verum
end;
then reconsider P = { A where A is Subset of T : ex B being Subset of T st
( A = Cl (Int (Cl B)) & B in F ) } as Subset-Family of T by TARSKI:def_3;
reconsider P = P as Subset-Family of T ;
for X being set holds
( X in Cl (Int (Cl F)) iff X in P )
proof
let X be set ; ::_thesis: ( X in Cl (Int (Cl F)) iff X in P )
A1: now__::_thesis:_(_X_in_P_implies_X_in_Cl_(Int_(Cl_F))_)
assume A2: X in P ; ::_thesis: X in Cl (Int (Cl F))
then reconsider C = X as Subset of T ;
ex D being Subset of T st
( D = C & ex B being Subset of T st
( D = Cl (Int (Cl B)) & B in F ) ) by A2;
then consider B being Subset of T such that
A3: C = Cl (Int (Cl B)) and
A4: B in F ;
Cl B in Cl F by A4, PCOMPS_1:def_2;
then Int (Cl B) in Int (Cl F) by Def1;
hence X in Cl (Int (Cl F)) by A3, PCOMPS_1:def_2; ::_thesis: verum
end;
now__::_thesis:_(_X_in_Cl_(Int_(Cl_F))_implies_X_in_P_)
assume A5: X in Cl (Int (Cl F)) ; ::_thesis: X in P
then reconsider C = X as Subset of T ;
consider B being Subset of T such that
A6: C = Cl B and
A7: B in Int (Cl F) by A5, PCOMPS_1:def_2;
consider D being Subset of T such that
A8: B = Int D and
A9: D in Cl F by A7, Def1;
ex E being Subset of T st
( D = Cl E & E in F ) by A9, PCOMPS_1:def_2;
hence X in P by A6, A8; ::_thesis: verum
end;
hence ( X in Cl (Int (Cl F)) iff X in P ) by A1; ::_thesis: verum
end;
hence Cl (Int (Cl F)) = { A where A is Subset of T : ex B being Subset of T st
( A = Cl (Int (Cl B)) & B in F ) } by TARSKI:1; ::_thesis: verum
end;
theorem Th34: :: TDLAT_2:34
for T being non empty TopSpace
for F being Subset-Family of T holds Int (Cl (Int F)) = { A where A is Subset of T : ex B being Subset of T st
( A = Int (Cl (Int B)) & B in F ) }
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds Int (Cl (Int F)) = { A where A is Subset of T : ex B being Subset of T st
( A = Int (Cl (Int B)) & B in F ) }
let F be Subset-Family of T; ::_thesis: Int (Cl (Int F)) = { A where A is Subset of T : ex B being Subset of T st
( A = Int (Cl (Int B)) & B in F ) }
set P = { A where A is Subset of T : ex B being Subset of T st
( A = Int (Cl (Int B)) & B in F ) } ;
now__::_thesis:_for_C_being_set_st_C_in__{__A_where_A_is_Subset_of_T_:_ex_B_being_Subset_of_T_st_
(_A_=_Int_(Cl_(Int_B))_&_B_in_F_)__}__holds_
C_in_bool_the_carrier_of_T
let C be set ; ::_thesis: ( C in { A where A is Subset of T : ex B being Subset of T st
( A = Int (Cl (Int B)) & B in F ) } implies C in bool the carrier of T )
assume C in { A where A is Subset of T : ex B being Subset of T st
( A = Int (Cl (Int B)) & B in F ) } ; ::_thesis: C in bool the carrier of T
then ex A being Subset of T st
( C = A & ex B being Subset of T st
( A = Int (Cl (Int B)) & B in F ) ) ;
hence C in bool the carrier of T ; ::_thesis: verum
end;
then reconsider P = { A where A is Subset of T : ex B being Subset of T st
( A = Int (Cl (Int B)) & B in F ) } as Subset-Family of T by TARSKI:def_3;
reconsider P = P as Subset-Family of T ;
for X being set holds
( X in Int (Cl (Int F)) iff X in P )
proof
let X be set ; ::_thesis: ( X in Int (Cl (Int F)) iff X in P )
A1: now__::_thesis:_(_X_in_P_implies_X_in_Int_(Cl_(Int_F))_)
assume A2: X in P ; ::_thesis: X in Int (Cl (Int F))
then reconsider C = X as Subset of T ;
ex D being Subset of T st
( D = C & ex B being Subset of T st
( D = Int (Cl (Int B)) & B in F ) ) by A2;
then consider B being Subset of T such that
A3: C = Int (Cl (Int B)) and
A4: B in F ;
Int B in Int F by A4, Def1;
then Cl (Int B) in Cl (Int F) by PCOMPS_1:def_2;
hence X in Int (Cl (Int F)) by A3, Def1; ::_thesis: verum
end;
now__::_thesis:_(_X_in_Int_(Cl_(Int_F))_implies_X_in_P_)
assume A5: X in Int (Cl (Int F)) ; ::_thesis: X in P
then reconsider C = X as Subset of T ;
consider B being Subset of T such that
A6: C = Int B and
A7: B in Cl (Int F) by A5, Def1;
consider D being Subset of T such that
A8: B = Cl D and
A9: D in Int F by A7, PCOMPS_1:def_2;
ex E being Subset of T st
( D = Int E & E in F ) by A9, Def1;
hence X in P by A6, A8; ::_thesis: verum
end;
hence ( X in Int (Cl (Int F)) iff X in P ) by A1; ::_thesis: verum
end;
hence Int (Cl (Int F)) = { A where A is Subset of T : ex B being Subset of T st
( A = Int (Cl (Int B)) & B in F ) } by TARSKI:1; ::_thesis: verum
end;
theorem :: TDLAT_2:35
for T being non empty TopSpace
for F being Subset-Family of T holds Cl (Int (Cl (Int F))) = Cl (Int F)
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds Cl (Int (Cl (Int F))) = Cl (Int F)
let F be Subset-Family of T; ::_thesis: Cl (Int (Cl (Int F))) = Cl (Int F)
set H = { A where A is Subset of T : ex B being Subset of T st
( A = Int (Cl (Int B)) & B in F ) } ;
Int (Cl (Int F)) = { A where A is Subset of T : ex B being Subset of T st
( A = Int (Cl (Int B)) & B in F ) } by Th34;
then reconsider H = { A where A is Subset of T : ex B being Subset of T st
( A = Int (Cl (Int B)) & B in F ) } as Subset-Family of T ;
A1: Cl (Int (Cl (Int F))) = Cl H by Th34;
A2: Cl (Int F) = { A where A is Subset of T : ex B being Subset of T st
( A = Cl (Int B) & B in F ) } by Th31;
for X being set holds
( X in Cl (Int (Cl (Int F))) iff X in Cl (Int F) )
proof
let X be set ; ::_thesis: ( X in Cl (Int (Cl (Int F))) iff X in Cl (Int F) )
A3: now__::_thesis:_(_X_in_Cl_(Int_F)_implies_X_in_Cl_(Int_(Cl_(Int_F)))_)
assume A4: X in Cl (Int F) ; ::_thesis: X in Cl (Int (Cl (Int F)))
then reconsider C = X as Subset of T ;
ex D being Subset of T st
( D = C & ex B being Subset of T st
( D = Cl (Int B) & B in F ) ) by A2, A4;
then consider B being Subset of T such that
A5: C = Cl (Int B) and
A6: B in F ;
Int B in Int F by A6, Def1;
then Cl (Int B) in Cl (Int F) by PCOMPS_1:def_2;
then A7: Int (Cl (Int B)) in Int (Cl (Int F)) by Def1;
C = Cl (Int (Cl (Int B))) by A5, TOPS_1:26;
hence X in Cl (Int (Cl (Int F))) by A7, PCOMPS_1:def_2; ::_thesis: verum
end;
now__::_thesis:_(_X_in_Cl_(Int_(Cl_(Int_F)))_implies_X_in_Cl_(Int_F)_)
assume A8: X in Cl (Int (Cl (Int F))) ; ::_thesis: X in Cl (Int F)
then reconsider C = X as Subset of T ;
consider B being Subset of T such that
A9: C = Cl B and
A10: B in { A where A is Subset of T : ex B being Subset of T st
( A = Int (Cl (Int B)) & B in F ) } by A1, A8, PCOMPS_1:def_2;
ex S being Subset of T st
( S = B & ex R being Subset of T st
( S = Int (Cl (Int R)) & R in F ) ) by A10;
then consider D being Subset of T such that
A11: B = Int (Cl (Int D)) and
A12: D in F ;
A13: Int D in Int F by A12, Def1;
C = Cl (Int D) by A9, A11, TOPS_1:26;
hence X in Cl (Int F) by A13, PCOMPS_1:def_2; ::_thesis: verum
end;
hence ( X in Cl (Int (Cl (Int F))) iff X in Cl (Int F) ) by A3; ::_thesis: verum
end;
hence Cl (Int (Cl (Int F))) = Cl (Int F) by TARSKI:1; ::_thesis: verum
end;
theorem :: TDLAT_2:36
for T being non empty TopSpace
for F being Subset-Family of T holds Int (Cl (Int (Cl F))) = Int (Cl F)
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds Int (Cl (Int (Cl F))) = Int (Cl F)
let F be Subset-Family of T; ::_thesis: Int (Cl (Int (Cl F))) = Int (Cl F)
set H = { A where A is Subset of T : ex B being Subset of T st
( A = Cl (Int (Cl B)) & B in F ) } ;
Cl (Int (Cl F)) = { A where A is Subset of T : ex B being Subset of T st
( A = Cl (Int (Cl B)) & B in F ) } by Th33;
then reconsider H = { A where A is Subset of T : ex B being Subset of T st
( A = Cl (Int (Cl B)) & B in F ) } as Subset-Family of T ;
A1: Int (Cl (Int (Cl F))) = Int H by Th33;
A2: Int (Cl F) = { A where A is Subset of T : ex B being Subset of T st
( A = Int (Cl B) & B in F ) } by Th32;
for X being set holds
( X in Int (Cl (Int (Cl F))) iff X in Int (Cl F) )
proof
let X be set ; ::_thesis: ( X in Int (Cl (Int (Cl F))) iff X in Int (Cl F) )
A3: now__::_thesis:_(_X_in_Int_(Cl_F)_implies_X_in_Int_(Cl_(Int_(Cl_F)))_)
assume A4: X in Int (Cl F) ; ::_thesis: X in Int (Cl (Int (Cl F)))
then reconsider C = X as Subset of T ;
ex D being Subset of T st
( D = C & ex B being Subset of T st
( D = Int (Cl B) & B in F ) ) by A2, A4;
then consider B being Subset of T such that
A5: C = Int (Cl B) and
A6: B in F ;
Cl B in Cl F by A6, PCOMPS_1:def_2;
then Int (Cl B) in Int (Cl F) by Def1;
then A7: Cl (Int (Cl B)) in Cl (Int (Cl F)) by PCOMPS_1:def_2;
C = Int (Cl (Int (Cl B))) by A5, TDLAT_1:5;
hence X in Int (Cl (Int (Cl F))) by A7, Def1; ::_thesis: verum
end;
now__::_thesis:_(_X_in_Int_(Cl_(Int_(Cl_F)))_implies_X_in_Int_(Cl_F)_)
assume A8: X in Int (Cl (Int (Cl F))) ; ::_thesis: X in Int (Cl F)
then reconsider C = X as Subset of T ;
consider B being Subset of T such that
A9: C = Int B and
A10: B in { A where A is Subset of T : ex B being Subset of T st
( A = Cl (Int (Cl B)) & B in F ) } by A1, A8, Def1;
ex S being Subset of T st
( S = B & ex R being Subset of T st
( S = Cl (Int (Cl R)) & R in F ) ) by A10;
then consider D being Subset of T such that
A11: B = Cl (Int (Cl D)) and
A12: D in F ;
A13: Cl D in Cl F by A12, PCOMPS_1:def_2;
C = Int (Cl D) by A9, A11, TDLAT_1:5;
hence X in Int (Cl F) by A13, Def1; ::_thesis: verum
end;
hence ( X in Int (Cl (Int (Cl F))) iff X in Int (Cl F) ) by A3; ::_thesis: verum
end;
hence Int (Cl (Int (Cl F))) = Int (Cl F) by TARSKI:1; ::_thesis: verum
end;
theorem :: TDLAT_2:37
for T being non empty TopSpace
for F being Subset-Family of T holds union (Int (Cl F)) c= union (Cl (Int (Cl F)))
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds union (Int (Cl F)) c= union (Cl (Int (Cl F)))
let F be Subset-Family of T; ::_thesis: union (Int (Cl F)) c= union (Cl (Int (Cl F)))
now__::_thesis:_for_x_being_set_st_x_in_union_(Int_(Cl_F))_holds_
x_in_union_(Cl_(Int_(Cl_F)))
let x be set ; ::_thesis: ( x in union (Int (Cl F)) implies x in union (Cl (Int (Cl F))) )
assume x in union (Int (Cl F)) ; ::_thesis: x in union (Cl (Int (Cl F)))
then consider A being set such that
A1: x in A and
A2: A in Int (Cl F) by TARSKI:def_4;
reconsider A = A as Subset of T by A2;
consider B being Subset of T such that
A3: A = Int B and
A4: B in Cl F by A2, Def1;
consider D being Subset of T such that
A5: B = Cl D and
A6: D in F by A4, PCOMPS_1:def_2;
ex P being set st
( x in P & P in Cl (Int (Cl F)) )
proof
take Cl (Int (Cl D)) ; ::_thesis: ( x in Cl (Int (Cl D)) & Cl (Int (Cl D)) in Cl (Int (Cl F)) )
Cl D in Cl F by A6, PCOMPS_1:def_2;
then A7: Int (Cl D) in Int (Cl F) by Def1;
A c= Cl (Int (Cl D)) by A3, A5, Th2;
hence ( x in Cl (Int (Cl D)) & Cl (Int (Cl D)) in Cl (Int (Cl F)) ) by A1, A7, PCOMPS_1:def_2; ::_thesis: verum
end;
hence x in union (Cl (Int (Cl F))) by TARSKI:def_4; ::_thesis: verum
end;
hence union (Int (Cl F)) c= union (Cl (Int (Cl F))) by TARSKI:def_3; ::_thesis: verum
end;
theorem :: TDLAT_2:38
for T being non empty TopSpace
for F being Subset-Family of T holds meet (Int (Cl F)) c= meet (Cl (Int (Cl F)))
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds meet (Int (Cl F)) c= meet (Cl (Int (Cl F)))
let F be Subset-Family of T; ::_thesis: meet (Int (Cl F)) c= meet (Cl (Int (Cl F)))
now__::_thesis:_meet_(Int_(Cl_F))_c=_meet_(Cl_(Int_(Cl_F)))
percases ( F = {} or F <> {} ) ;
suppose F = {} ; ::_thesis: meet (Int (Cl F)) c= meet (Cl (Int (Cl F)))
then Cl F = {} by Th9;
then Int (Cl F) = {} by Th19;
hence meet (Int (Cl F)) c= meet (Cl (Int (Cl F))) by Th9; ::_thesis: verum
end;
suppose F <> {} ; ::_thesis: meet (Int (Cl F)) c= meet (Cl (Int (Cl F)))
then Cl F <> {} by Th9;
then Int (Cl F) <> {} by Th19;
then A1: Cl (Int (Cl F)) <> {} by Th9;
now__::_thesis:_for_x_being_set_st_x_in_meet_(Int_(Cl_F))_holds_
x_in_meet_(Cl_(Int_(Cl_F)))
let x be set ; ::_thesis: ( x in meet (Int (Cl F)) implies x in meet (Cl (Int (Cl F))) )
assume A2: x in meet (Int (Cl F)) ; ::_thesis: x in meet (Cl (Int (Cl F)))
for A being set st A in Cl (Int (Cl F)) holds
x in A
proof
let A be set ; ::_thesis: ( A in Cl (Int (Cl F)) implies x in A )
assume A3: A in Cl (Int (Cl F)) ; ::_thesis: x in A
then reconsider A = A as Subset of T ;
consider B being Subset of T such that
A4: A = Cl B and
A5: B in Int (Cl F) by A3, PCOMPS_1:def_2;
A6: B c= Cl B by PRE_TOPC:18;
x in B by A2, A5, SETFAM_1:def_1;
hence x in A by A4, A6; ::_thesis: verum
end;
hence x in meet (Cl (Int (Cl F))) by A1, SETFAM_1:def_1; ::_thesis: verum
end;
hence meet (Int (Cl F)) c= meet (Cl (Int (Cl F))) by TARSKI:def_3; ::_thesis: verum
end;
end;
end;
hence meet (Int (Cl F)) c= meet (Cl (Int (Cl F))) ; ::_thesis: verum
end;
theorem :: TDLAT_2:39
for T being non empty TopSpace
for F being Subset-Family of T holds union (Cl (Int F)) c= union (Cl (Int (Cl F)))
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds union (Cl (Int F)) c= union (Cl (Int (Cl F)))
let F be Subset-Family of T; ::_thesis: union (Cl (Int F)) c= union (Cl (Int (Cl F)))
now__::_thesis:_for_x_being_set_st_x_in_union_(Cl_(Int_F))_holds_
x_in_union_(Cl_(Int_(Cl_F)))
let x be set ; ::_thesis: ( x in union (Cl (Int F)) implies x in union (Cl (Int (Cl F))) )
assume x in union (Cl (Int F)) ; ::_thesis: x in union (Cl (Int (Cl F)))
then consider A being set such that
A1: x in A and
A2: A in Cl (Int F) by TARSKI:def_4;
reconsider A = A as Subset of T by A2;
consider B being Subset of T such that
A3: A = Cl B and
A4: B in Int F by A2, PCOMPS_1:def_2;
consider D being Subset of T such that
A5: B = Int D and
A6: D in F by A4, Def1;
ex P being set st
( x in P & P in Cl (Int (Cl F)) )
proof
take Cl (Int (Cl D)) ; ::_thesis: ( x in Cl (Int (Cl D)) & Cl (Int (Cl D)) in Cl (Int (Cl F)) )
Cl D in Cl F by A6, PCOMPS_1:def_2;
then A7: Int (Cl D) in Int (Cl F) by Def1;
A c= Cl (Int (Cl D)) by A3, A5, Th2;
hence ( x in Cl (Int (Cl D)) & Cl (Int (Cl D)) in Cl (Int (Cl F)) ) by A1, A7, PCOMPS_1:def_2; ::_thesis: verum
end;
hence x in union (Cl (Int (Cl F))) by TARSKI:def_4; ::_thesis: verum
end;
hence union (Cl (Int F)) c= union (Cl (Int (Cl F))) by TARSKI:def_3; ::_thesis: verum
end;
theorem :: TDLAT_2:40
for T being non empty TopSpace
for F being Subset-Family of T holds meet (Cl (Int F)) c= meet (Cl (Int (Cl F)))
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds meet (Cl (Int F)) c= meet (Cl (Int (Cl F)))
let F be Subset-Family of T; ::_thesis: meet (Cl (Int F)) c= meet (Cl (Int (Cl F)))
now__::_thesis:_meet_(Cl_(Int_F))_c=_meet_(Cl_(Int_(Cl_F)))
percases ( F = {} or F <> {} ) ;
suppose F = {} ; ::_thesis: meet (Cl (Int F)) c= meet (Cl (Int (Cl F)))
hence meet (Cl (Int F)) c= meet (Cl (Int (Cl F))) by Th9; ::_thesis: verum
end;
suppose F <> {} ; ::_thesis: meet (Cl (Int F)) c= meet (Cl (Int (Cl F)))
then Cl F <> {} by Th9;
then Int (Cl F) <> {} by Th19;
then A1: Cl (Int (Cl F)) <> {} by Th9;
now__::_thesis:_for_x_being_set_st_x_in_meet_(Cl_(Int_F))_holds_
x_in_meet_(Cl_(Int_(Cl_F)))
let x be set ; ::_thesis: ( x in meet (Cl (Int F)) implies x in meet (Cl (Int (Cl F))) )
assume A2: x in meet (Cl (Int F)) ; ::_thesis: x in meet (Cl (Int (Cl F)))
for A being set st A in Cl (Int (Cl F)) holds
x in A
proof
let A be set ; ::_thesis: ( A in Cl (Int (Cl F)) implies x in A )
assume A3: A in Cl (Int (Cl F)) ; ::_thesis: x in A
then reconsider A = A as Subset of T ;
consider B being Subset of T such that
A4: A = Cl B and
A5: B in Int (Cl F) by A3, PCOMPS_1:def_2;
consider D being Subset of T such that
A6: B = Int D and
A7: D in Cl F by A5, Def1;
consider E being Subset of T such that
A8: D = Cl E and
A9: E in F by A7, PCOMPS_1:def_2;
Int E in Int F by A9, Def1;
then Cl (Int E) in Cl (Int F) by PCOMPS_1:def_2;
then A10: x in Cl (Int E) by A2, SETFAM_1:def_1;
Cl (Int E) c= Cl (Int (Cl E)) by Th2;
hence x in A by A4, A6, A8, A10; ::_thesis: verum
end;
hence x in meet (Cl (Int (Cl F))) by A1, SETFAM_1:def_1; ::_thesis: verum
end;
hence meet (Cl (Int F)) c= meet (Cl (Int (Cl F))) by TARSKI:def_3; ::_thesis: verum
end;
end;
end;
hence meet (Cl (Int F)) c= meet (Cl (Int (Cl F))) ; ::_thesis: verum
end;
theorem :: TDLAT_2:41
for T being non empty TopSpace
for F being Subset-Family of T holds union (Int (Cl (Int F))) c= union (Int (Cl F))
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds union (Int (Cl (Int F))) c= union (Int (Cl F))
let F be Subset-Family of T; ::_thesis: union (Int (Cl (Int F))) c= union (Int (Cl F))
now__::_thesis:_for_x_being_set_st_x_in_union_(Int_(Cl_(Int_F)))_holds_
x_in_union_(Int_(Cl_F))
let x be set ; ::_thesis: ( x in union (Int (Cl (Int F))) implies x in union (Int (Cl F)) )
assume x in union (Int (Cl (Int F))) ; ::_thesis: x in union (Int (Cl F))
then consider A being set such that
A1: x in A and
A2: A in Int (Cl (Int F)) by TARSKI:def_4;
reconsider A = A as Subset of T by A2;
consider B being Subset of T such that
A3: A = Int B and
A4: B in Cl (Int F) by A2, Def1;
consider D being Subset of T such that
A5: B = Cl D and
A6: D in Int F by A4, PCOMPS_1:def_2;
consider E being Subset of T such that
A7: D = Int E and
A8: E in F by A6, Def1;
ex P being set st
( x in P & P in Int (Cl F) )
proof
take Int (Cl E) ; ::_thesis: ( x in Int (Cl E) & Int (Cl E) in Int (Cl F) )
A9: Cl E in Cl F by A8, PCOMPS_1:def_2;
A c= Int (Cl E) by A3, A5, A7, Th1;
hence ( x in Int (Cl E) & Int (Cl E) in Int (Cl F) ) by A1, A9, Def1; ::_thesis: verum
end;
hence x in union (Int (Cl F)) by TARSKI:def_4; ::_thesis: verum
end;
hence union (Int (Cl (Int F))) c= union (Int (Cl F)) by TARSKI:def_3; ::_thesis: verum
end;
theorem :: TDLAT_2:42
for T being non empty TopSpace
for F being Subset-Family of T holds meet (Int (Cl (Int F))) c= meet (Int (Cl F))
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds meet (Int (Cl (Int F))) c= meet (Int (Cl F))
let F be Subset-Family of T; ::_thesis: meet (Int (Cl (Int F))) c= meet (Int (Cl F))
now__::_thesis:_meet_(Int_(Cl_(Int_F)))_c=_meet_(Int_(Cl_F))
percases ( F = {} or F <> {} ) ;
suppose F = {} ; ::_thesis: meet (Int (Cl (Int F))) c= meet (Int (Cl F))
hence meet (Int (Cl (Int F))) c= meet (Int (Cl F)) by Th19; ::_thesis: verum
end;
suppose F <> {} ; ::_thesis: meet (Int (Cl (Int F))) c= meet (Int (Cl F))
then Cl F <> {} by Th9;
then A1: Int (Cl F) <> {} by Th19;
now__::_thesis:_for_x_being_set_st_x_in_meet_(Int_(Cl_(Int_F)))_holds_
x_in_meet_(Int_(Cl_F))
let x be set ; ::_thesis: ( x in meet (Int (Cl (Int F))) implies x in meet (Int (Cl F)) )
assume A2: x in meet (Int (Cl (Int F))) ; ::_thesis: x in meet (Int (Cl F))
for A being set st A in Int (Cl F) holds
x in A
proof
let A be set ; ::_thesis: ( A in Int (Cl F) implies x in A )
assume A3: A in Int (Cl F) ; ::_thesis: x in A
then reconsider A = A as Subset of T ;
consider E being Subset of T such that
A4: A = Int E and
A5: E in Cl F by A3, Def1;
consider B being Subset of T such that
A6: E = Cl B and
A7: B in F by A5, PCOMPS_1:def_2;
Int B in Int F by A7, Def1;
then Cl (Int B) in Cl (Int F) by PCOMPS_1:def_2;
then Int (Cl (Int B)) in Int (Cl (Int F)) by Def1;
then A8: x in Int (Cl (Int B)) by A2, SETFAM_1:def_1;
Int (Cl (Int B)) c= Int (Cl B) by Th1;
hence x in A by A4, A6, A8; ::_thesis: verum
end;
hence x in meet (Int (Cl F)) by A1, SETFAM_1:def_1; ::_thesis: verum
end;
hence meet (Int (Cl (Int F))) c= meet (Int (Cl F)) by TARSKI:def_3; ::_thesis: verum
end;
end;
end;
hence meet (Int (Cl (Int F))) c= meet (Int (Cl F)) ; ::_thesis: verum
end;
theorem :: TDLAT_2:43
for T being non empty TopSpace
for F being Subset-Family of T holds union (Int (Cl (Int F))) c= union (Cl (Int F))
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds union (Int (Cl (Int F))) c= union (Cl (Int F))
let F be Subset-Family of T; ::_thesis: union (Int (Cl (Int F))) c= union (Cl (Int F))
now__::_thesis:_for_x_being_set_st_x_in_union_(Int_(Cl_(Int_F)))_holds_
x_in_union_(Cl_(Int_F))
let x be set ; ::_thesis: ( x in union (Int (Cl (Int F))) implies x in union (Cl (Int F)) )
assume x in union (Int (Cl (Int F))) ; ::_thesis: x in union (Cl (Int F))
then consider A being set such that
A1: x in A and
A2: A in Int (Cl (Int F)) by TARSKI:def_4;
reconsider A = A as Subset of T by A2;
consider B being Subset of T such that
A3: A = Int B and
A4: B in Cl (Int F) by A2, Def1;
consider D being Subset of T such that
A5: B = Cl D and
A6: D in Int F by A4, PCOMPS_1:def_2;
consider E being Subset of T such that
A7: D = Int E and
A8: E in F by A6, Def1;
ex P being set st
( x in P & P in Cl (Int F) )
proof
take Cl (Int E) ; ::_thesis: ( x in Cl (Int E) & Cl (Int E) in Cl (Int F) )
A9: Int E in Int F by A8, Def1;
A c= Cl (Int E) by A3, A5, A7, Th1;
hence ( x in Cl (Int E) & Cl (Int E) in Cl (Int F) ) by A1, A9, PCOMPS_1:def_2; ::_thesis: verum
end;
hence x in union (Cl (Int F)) by TARSKI:def_4; ::_thesis: verum
end;
hence union (Int (Cl (Int F))) c= union (Cl (Int F)) by TARSKI:def_3; ::_thesis: verum
end;
theorem :: TDLAT_2:44
for T being non empty TopSpace
for F being Subset-Family of T holds meet (Int (Cl (Int F))) c= meet (Cl (Int F))
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds meet (Int (Cl (Int F))) c= meet (Cl (Int F))
let F be Subset-Family of T; ::_thesis: meet (Int (Cl (Int F))) c= meet (Cl (Int F))
now__::_thesis:_meet_(Int_(Cl_(Int_F)))_c=_meet_(Cl_(Int_F))
percases ( F = {} or F <> {} ) ;
suppose F = {} ; ::_thesis: meet (Int (Cl (Int F))) c= meet (Cl (Int F))
then Int F = {} by Th19;
then Cl (Int F) = {} by Th9;
hence meet (Int (Cl (Int F))) c= meet (Cl (Int F)) by Th19; ::_thesis: verum
end;
suppose F <> {} ; ::_thesis: meet (Int (Cl (Int F))) c= meet (Cl (Int F))
then Int F <> {} by Th19;
then A1: Cl (Int F) <> {} by Th9;
now__::_thesis:_for_x_being_set_st_x_in_meet_(Int_(Cl_(Int_F)))_holds_
x_in_meet_(Cl_(Int_F))
let x be set ; ::_thesis: ( x in meet (Int (Cl (Int F))) implies x in meet (Cl (Int F)) )
assume A2: x in meet (Int (Cl (Int F))) ; ::_thesis: x in meet (Cl (Int F))
for A being set st A in Cl (Int F) holds
x in A
proof
let A be set ; ::_thesis: ( A in Cl (Int F) implies x in A )
assume A3: A in Cl (Int F) ; ::_thesis: x in A
then reconsider A = A as Subset of T ;
consider E being Subset of T such that
A4: A = Cl E and
A5: E in Int F by A3, PCOMPS_1:def_2;
consider B being Subset of T such that
A6: E = Int B and
A7: B in F by A5, Def1;
Int B in Int F by A7, Def1;
then Cl (Int B) in Cl (Int F) by PCOMPS_1:def_2;
then Int (Cl (Int B)) in Int (Cl (Int F)) by Def1;
then A8: x in Int (Cl (Int B)) by A2, SETFAM_1:def_1;
Int (Cl (Int B)) c= Cl (Int B) by Th1;
hence x in A by A4, A6, A8; ::_thesis: verum
end;
hence x in meet (Cl (Int F)) by A1, SETFAM_1:def_1; ::_thesis: verum
end;
hence meet (Int (Cl (Int F))) c= meet (Cl (Int F)) by TARSKI:def_3; ::_thesis: verum
end;
end;
end;
hence meet (Int (Cl (Int F))) c= meet (Cl (Int F)) ; ::_thesis: verum
end;
theorem :: TDLAT_2:45
for T being non empty TopSpace
for F being Subset-Family of T holds union (Cl (Int (Cl F))) c= union (Cl F)
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds union (Cl (Int (Cl F))) c= union (Cl F)
let F be Subset-Family of T; ::_thesis: union (Cl (Int (Cl F))) c= union (Cl F)
now__::_thesis:_for_x_being_set_st_x_in_union_(Cl_(Int_(Cl_F)))_holds_
x_in_union_(Cl_F)
let x be set ; ::_thesis: ( x in union (Cl (Int (Cl F))) implies x in union (Cl F) )
assume x in union (Cl (Int (Cl F))) ; ::_thesis: x in union (Cl F)
then consider A being set such that
A1: x in A and
A2: A in Cl (Int (Cl F)) by TARSKI:def_4;
reconsider A = A as Subset of T by A2;
consider B being Subset of T such that
A3: A = Cl B and
A4: B in Int (Cl F) by A2, PCOMPS_1:def_2;
consider D being Subset of T such that
A5: B = Int D and
A6: D in Cl F by A4, Def1;
consider E being Subset of T such that
A7: D = Cl E and
A8: E in F by A6, PCOMPS_1:def_2;
ex P being set st
( x in P & P in Cl F )
proof
take Cl E ; ::_thesis: ( x in Cl E & Cl E in Cl F )
A c= Cl E by A3, A5, A7, TDLAT_1:3;
hence ( x in Cl E & Cl E in Cl F ) by A1, A8, PCOMPS_1:def_2; ::_thesis: verum
end;
hence x in union (Cl F) by TARSKI:def_4; ::_thesis: verum
end;
hence union (Cl (Int (Cl F))) c= union (Cl F) by TARSKI:def_3; ::_thesis: verum
end;
theorem :: TDLAT_2:46
for T being non empty TopSpace
for F being Subset-Family of T holds meet (Cl (Int (Cl F))) c= meet (Cl F)
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds meet (Cl (Int (Cl F))) c= meet (Cl F)
let F be Subset-Family of T; ::_thesis: meet (Cl (Int (Cl F))) c= meet (Cl F)
now__::_thesis:_meet_(Cl_(Int_(Cl_F)))_c=_meet_(Cl_F)
percases ( F = {} or F <> {} ) ;
supposeA1: F = {} ; ::_thesis: meet (Cl (Int (Cl F))) c= meet (Cl F)
then Cl F = {} by Th9;
hence meet (Cl (Int (Cl F))) c= meet (Cl F) by A1, Th19; ::_thesis: verum
end;
suppose F <> {} ; ::_thesis: meet (Cl (Int (Cl F))) c= meet (Cl F)
then A2: Cl F <> {} by Th9;
now__::_thesis:_for_x_being_set_st_x_in_meet_(Cl_(Int_(Cl_F)))_holds_
x_in_meet_(Cl_F)
let x be set ; ::_thesis: ( x in meet (Cl (Int (Cl F))) implies x in meet (Cl F) )
assume A3: x in meet (Cl (Int (Cl F))) ; ::_thesis: x in meet (Cl F)
for A being set st A in Cl F holds
x in A
proof
let A be set ; ::_thesis: ( A in Cl F implies x in A )
assume A4: A in Cl F ; ::_thesis: x in A
then reconsider A = A as Subset of T ;
consider B being Subset of T such that
A5: A = Cl B and
A6: B in F by A4, PCOMPS_1:def_2;
Cl B in Cl F by A6, PCOMPS_1:def_2;
then Int (Cl B) in Int (Cl F) by Def1;
then Cl (Int (Cl B)) in Cl (Int (Cl F)) by PCOMPS_1:def_2;
then A7: x in Cl (Int (Cl B)) by A3, SETFAM_1:def_1;
Cl (Int (Cl B)) c= Cl B by TDLAT_1:3;
hence x in A by A5, A7; ::_thesis: verum
end;
hence x in meet (Cl F) by A2, SETFAM_1:def_1; ::_thesis: verum
end;
hence meet (Cl (Int (Cl F))) c= meet (Cl F) by TARSKI:def_3; ::_thesis: verum
end;
end;
end;
hence meet (Cl (Int (Cl F))) c= meet (Cl F) ; ::_thesis: verum
end;
theorem :: TDLAT_2:47
for T being non empty TopSpace
for F being Subset-Family of T holds union (Int F) c= union (Int (Cl (Int F)))
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds union (Int F) c= union (Int (Cl (Int F)))
let F be Subset-Family of T; ::_thesis: union (Int F) c= union (Int (Cl (Int F)))
now__::_thesis:_for_x_being_set_st_x_in_union_(Int_F)_holds_
x_in_union_(Int_(Cl_(Int_F)))
let x be set ; ::_thesis: ( x in union (Int F) implies x in union (Int (Cl (Int F))) )
assume x in union (Int F) ; ::_thesis: x in union (Int (Cl (Int F)))
then consider A being set such that
A1: x in A and
A2: A in Int F by TARSKI:def_4;
reconsider A = A as Subset of T by A2;
consider B being Subset of T such that
A3: A = Int B and
A4: B in F by A2, Def1;
ex P being set st
( x in P & P in Int (Cl (Int F)) )
proof
take Int (Cl (Int B)) ; ::_thesis: ( x in Int (Cl (Int B)) & Int (Cl (Int B)) in Int (Cl (Int F)) )
Int B in Int F by A4, Def1;
then A5: Cl (Int B) in Cl (Int F) by PCOMPS_1:def_2;
A c= Int (Cl (Int B)) by A3, TDLAT_1:4;
hence ( x in Int (Cl (Int B)) & Int (Cl (Int B)) in Int (Cl (Int F)) ) by A1, A5, Def1; ::_thesis: verum
end;
hence x in union (Int (Cl (Int F))) by TARSKI:def_4; ::_thesis: verum
end;
hence union (Int F) c= union (Int (Cl (Int F))) by TARSKI:def_3; ::_thesis: verum
end;
theorem :: TDLAT_2:48
for T being non empty TopSpace
for F being Subset-Family of T holds meet (Int F) c= meet (Int (Cl (Int F)))
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds meet (Int F) c= meet (Int (Cl (Int F)))
let F be Subset-Family of T; ::_thesis: meet (Int F) c= meet (Int (Cl (Int F)))
now__::_thesis:_meet_(Int_F)_c=_meet_(Int_(Cl_(Int_F)))
percases ( F = {} or F <> {} ) ;
supposeA1: F = {} ; ::_thesis: meet (Int F) c= meet (Int (Cl (Int F)))
then Int F = {} by Th19;
hence meet (Int F) c= meet (Int (Cl (Int F))) by A1, Th9; ::_thesis: verum
end;
suppose F <> {} ; ::_thesis: meet (Int F) c= meet (Int (Cl (Int F)))
then Int F <> {} by Th19;
then Cl (Int F) <> {} by Th9;
then A2: Int (Cl (Int F)) <> {} by Th19;
now__::_thesis:_for_x_being_set_st_x_in_meet_(Int_F)_holds_
x_in_meet_(Int_(Cl_(Int_F)))
let x be set ; ::_thesis: ( x in meet (Int F) implies x in meet (Int (Cl (Int F))) )
assume A3: x in meet (Int F) ; ::_thesis: x in meet (Int (Cl (Int F)))
for A being set st A in Int (Cl (Int F)) holds
x in A
proof
let A be set ; ::_thesis: ( A in Int (Cl (Int F)) implies x in A )
assume A4: A in Int (Cl (Int F)) ; ::_thesis: x in A
then reconsider A = A as Subset of T ;
consider E being Subset of T such that
A5: A = Int E and
A6: E in Cl (Int F) by A4, Def1;
consider B being Subset of T such that
A7: E = Cl B and
A8: B in Int F by A6, PCOMPS_1:def_2;
consider D being Subset of T such that
A9: B = Int D and
A10: D in F by A8, Def1;
Int D in Int F by A10, Def1;
then A11: x in Int D by A3, SETFAM_1:def_1;
Int D c= Int (Cl (Int D)) by TDLAT_1:4;
hence x in A by A5, A7, A9, A11; ::_thesis: verum
end;
hence x in meet (Int (Cl (Int F))) by A2, SETFAM_1:def_1; ::_thesis: verum
end;
hence meet (Int F) c= meet (Int (Cl (Int F))) by TARSKI:def_3; ::_thesis: verum
end;
end;
end;
hence meet (Int F) c= meet (Int (Cl (Int F))) ; ::_thesis: verum
end;
theorem Th49: :: TDLAT_2:49
for T being non empty TopSpace
for F being Subset-Family of T holds union (Cl (Int F)) c= Cl (Int (union F))
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds union (Cl (Int F)) c= Cl (Int (union F))
let F be Subset-Family of T; ::_thesis: union (Cl (Int F)) c= Cl (Int (union F))
A1: Cl (union (Int F)) c= Cl (Int (union F)) by Th28, PRE_TOPC:19;
union (Cl (Int F)) c= Cl (union (Int F)) by Th15;
hence union (Cl (Int F)) c= Cl (Int (union F)) by A1, XBOOLE_1:1; ::_thesis: verum
end;
theorem Th50: :: TDLAT_2:50
for T being non empty TopSpace
for F being Subset-Family of T holds Cl (Int (meet F)) c= meet (Cl (Int F))
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds Cl (Int (meet F)) c= meet (Cl (Int F))
let F be Subset-Family of T; ::_thesis: Cl (Int (meet F)) c= meet (Cl (Int F))
A1: Cl (meet (Int F)) c= meet (Cl (Int F)) by Th14;
Cl (Int (meet F)) c= Cl (meet (Int F)) by Th29, PRE_TOPC:19;
hence Cl (Int (meet F)) c= meet (Cl (Int F)) by A1, XBOOLE_1:1; ::_thesis: verum
end;
theorem Th51: :: TDLAT_2:51
for T being non empty TopSpace
for F being Subset-Family of T holds union (Int (Cl F)) c= Int (Cl (union F))
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds union (Int (Cl F)) c= Int (Cl (union F))
let F be Subset-Family of T; ::_thesis: union (Int (Cl F)) c= Int (Cl (union F))
A1: Int (union (Cl F)) c= Int (Cl (union F)) by Th15, TOPS_1:19;
union (Int (Cl F)) c= Int (union (Cl F)) by Th28;
hence union (Int (Cl F)) c= Int (Cl (union F)) by A1, XBOOLE_1:1; ::_thesis: verum
end;
theorem Th52: :: TDLAT_2:52
for T being non empty TopSpace
for F being Subset-Family of T holds Int (Cl (meet F)) c= meet (Int (Cl F))
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds Int (Cl (meet F)) c= meet (Int (Cl F))
let F be Subset-Family of T; ::_thesis: Int (Cl (meet F)) c= meet (Int (Cl F))
A1: Int (meet (Cl F)) c= meet (Int (Cl F)) by Th29;
Int (Cl (meet F)) c= Int (meet (Cl F)) by Th14, TOPS_1:19;
hence Int (Cl (meet F)) c= meet (Int (Cl F)) by A1, XBOOLE_1:1; ::_thesis: verum
end;
theorem :: TDLAT_2:53
for T being non empty TopSpace
for F being Subset-Family of T holds union (Cl (Int (Cl F))) c= Cl (Int (Cl (union F)))
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds union (Cl (Int (Cl F))) c= Cl (Int (Cl (union F)))
let F be Subset-Family of T; ::_thesis: union (Cl (Int (Cl F))) c= Cl (Int (Cl (union F)))
A1: Cl (union (Int (Cl F))) c= Cl (Int (Cl (union F))) by Th51, PRE_TOPC:19;
union (Cl (Int (Cl F))) c= Cl (union (Int (Cl F))) by Th15;
hence union (Cl (Int (Cl F))) c= Cl (Int (Cl (union F))) by A1, XBOOLE_1:1; ::_thesis: verum
end;
theorem :: TDLAT_2:54
for T being non empty TopSpace
for F being Subset-Family of T holds Cl (Int (Cl (meet F))) c= meet (Cl (Int (Cl F)))
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds Cl (Int (Cl (meet F))) c= meet (Cl (Int (Cl F)))
let F be Subset-Family of T; ::_thesis: Cl (Int (Cl (meet F))) c= meet (Cl (Int (Cl F)))
A1: Cl (Int (Cl (meet F))) c= Cl (meet (Int (Cl F))) by Th52, PRE_TOPC:19;
Cl (meet (Int (Cl F))) c= meet (Cl (Int (Cl F))) by Th14;
hence Cl (Int (Cl (meet F))) c= meet (Cl (Int (Cl F))) by A1, XBOOLE_1:1; ::_thesis: verum
end;
theorem :: TDLAT_2:55
for T being non empty TopSpace
for F being Subset-Family of T holds union (Int (Cl (Int F))) c= Int (Cl (Int (union F)))
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds union (Int (Cl (Int F))) c= Int (Cl (Int (union F)))
let F be Subset-Family of T; ::_thesis: union (Int (Cl (Int F))) c= Int (Cl (Int (union F)))
A1: Int (union (Cl (Int F))) c= Int (Cl (Int (union F))) by Th49, TOPS_1:19;
union (Int (Cl (Int F))) c= Int (union (Cl (Int F))) by Th28;
hence union (Int (Cl (Int F))) c= Int (Cl (Int (union F))) by A1, XBOOLE_1:1; ::_thesis: verum
end;
theorem :: TDLAT_2:56
for T being non empty TopSpace
for F being Subset-Family of T holds Int (Cl (Int (meet F))) c= meet (Int (Cl (Int F)))
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds Int (Cl (Int (meet F))) c= meet (Int (Cl (Int F)))
let F be Subset-Family of T; ::_thesis: Int (Cl (Int (meet F))) c= meet (Int (Cl (Int F)))
A1: Int (Cl (Int (meet F))) c= Int (meet (Cl (Int F))) by Th50, TOPS_1:19;
Int (meet (Cl (Int F))) c= meet (Int (Cl (Int F))) by Th29;
hence Int (Cl (Int (meet F))) c= meet (Int (Cl (Int F))) by A1, XBOOLE_1:1; ::_thesis: verum
end;
theorem Th57: :: TDLAT_2:57
for T being non empty TopSpace
for F being Subset-Family of T st ( for A being Subset of T st A in F holds
A c= Cl (Int A) ) holds
( union F c= Cl (Int (union F)) & Cl (union F) = Cl (Int (Cl (union F))) )
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st ( for A being Subset of T st A in F holds
A c= Cl (Int A) ) holds
( union F c= Cl (Int (union F)) & Cl (union F) = Cl (Int (Cl (union F))) )
let F be Subset-Family of T; ::_thesis: ( ( for A being Subset of T st A in F holds
A c= Cl (Int A) ) implies ( union F c= Cl (Int (union F)) & Cl (union F) = Cl (Int (Cl (union F))) ) )
A1: Cl (Int (Cl (union F))) c= Cl (Cl (union F)) by PRE_TOPC:19, TOPS_1:16;
assume A2: for A being Subset of T st A in F holds
A c= Cl (Int A) ; ::_thesis: ( union F c= Cl (Int (union F)) & Cl (union F) = Cl (Int (Cl (union F))) )
A3: now__::_thesis:_for_A0_being_set_st_A0_in_F_holds_
A0_c=_Cl_(Int_(union_F))
let A0 be set ; ::_thesis: ( A0 in F implies A0 c= Cl (Int (union F)) )
assume A4: A0 in F ; ::_thesis: A0 c= Cl (Int (union F))
then reconsider A = A0 as Subset of T ;
Int A c= Int (union F) by A4, TOPS_1:19, ZFMISC_1:74;
then A5: Cl (Int A) c= Cl (Int (union F)) by PRE_TOPC:19;
A c= Cl (Int A) by A2, A4;
hence A0 c= Cl (Int (union F)) by A5, XBOOLE_1:1; ::_thesis: verum
end;
hence union F c= Cl (Int (union F)) by ZFMISC_1:76; ::_thesis: Cl (union F) = Cl (Int (Cl (union F)))
Int (union F) c= Int (Cl (union F)) by PRE_TOPC:18, TOPS_1:19;
then A6: Cl (Int (union F)) c= Cl (Int (Cl (union F))) by PRE_TOPC:19;
union F c= Cl (Int (union F)) by A3, ZFMISC_1:76;
then Cl (union F) c= Cl (Cl (Int (union F))) by PRE_TOPC:19;
then Cl (union F) c= Cl (Int (Cl (union F))) by A6, XBOOLE_1:1;
hence Cl (union F) = Cl (Int (Cl (union F))) by A1, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th58: :: TDLAT_2:58
for T being non empty TopSpace
for F being Subset-Family of T st ( for A being Subset of T st A in F holds
Int (Cl A) c= A ) holds
( Int (Cl (meet F)) c= meet F & Int (Cl (Int (meet F))) = Int (meet F) )
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st ( for A being Subset of T st A in F holds
Int (Cl A) c= A ) holds
( Int (Cl (meet F)) c= meet F & Int (Cl (Int (meet F))) = Int (meet F) )
let F be Subset-Family of T; ::_thesis: ( ( for A being Subset of T st A in F holds
Int (Cl A) c= A ) implies ( Int (Cl (meet F)) c= meet F & Int (Cl (Int (meet F))) = Int (meet F) ) )
A1: Int (Int (meet F)) c= Int (Cl (Int (meet F))) by PRE_TOPC:18, TOPS_1:19;
assume A2: for A being Subset of T st A in F holds
Int (Cl A) c= A ; ::_thesis: ( Int (Cl (meet F)) c= meet F & Int (Cl (Int (meet F))) = Int (meet F) )
thus Int (Cl (meet F)) c= meet F ::_thesis: Int (Cl (Int (meet F))) = Int (meet F)
proof
now__::_thesis:_Int_(Cl_(meet_F))_c=_meet_F
percases ( F = {} or F <> {} ) ;
supposeA3: F = {} ; ::_thesis: Int (Cl (meet F)) c= meet F
Cl ({} T) = {} T by PRE_TOPC:22;
hence Int (Cl (meet F)) c= meet F by A3, SETFAM_1:1; ::_thesis: verum
end;
supposeA4: F <> {} ; ::_thesis: Int (Cl (meet F)) c= meet F
now__::_thesis:_for_A0_being_set_st_A0_in_F_holds_
Int_(Cl_(meet_F))_c=_A0
let A0 be set ; ::_thesis: ( A0 in F implies Int (Cl (meet F)) c= A0 )
assume A5: A0 in F ; ::_thesis: Int (Cl (meet F)) c= A0
then reconsider A = A0 as Subset of T ;
Cl (meet F) c= Cl A by A5, PRE_TOPC:19, SETFAM_1:3;
then A6: Int (Cl (meet F)) c= Int (Cl A) by TOPS_1:19;
Int (Cl A) c= A by A2, A5;
hence Int (Cl (meet F)) c= A0 by A6, XBOOLE_1:1; ::_thesis: verum
end;
hence Int (Cl (meet F)) c= meet F by A4, SETFAM_1:5; ::_thesis: verum
end;
end;
end;
hence Int (Cl (meet F)) c= meet F ; ::_thesis: verum
end;
then A7: Int (Int (Cl (meet F))) c= Int (meet F) by TOPS_1:19;
Cl (Int (meet F)) c= Cl (meet F) by PRE_TOPC:19, TOPS_1:16;
then Int (Cl (Int (meet F))) c= Int (Cl (meet F)) by TOPS_1:19;
then Int (Cl (Int (meet F))) c= Int (meet F) by A7, XBOOLE_1:1;
hence Int (Cl (Int (meet F))) = Int (meet F) by A1, XBOOLE_0:def_10; ::_thesis: verum
end;
begin
theorem Th59: :: TDLAT_2:59
for T being non empty TopSpace
for A, B being Subset of T st B is condensed holds
( (Int (Cl (A \/ B))) \/ (A \/ B) = B iff A c= B )
proof
let T be non empty TopSpace; ::_thesis: for A, B being Subset of T st B is condensed holds
( (Int (Cl (A \/ B))) \/ (A \/ B) = B iff A c= B )
let A, B be Subset of T; ::_thesis: ( B is condensed implies ( (Int (Cl (A \/ B))) \/ (A \/ B) = B iff A c= B ) )
assume A1: B is condensed ; ::_thesis: ( (Int (Cl (A \/ B))) \/ (A \/ B) = B iff A c= B )
thus ( (Int (Cl (A \/ B))) \/ (A \/ B) = B implies A c= B ) ::_thesis: ( A c= B implies (Int (Cl (A \/ B))) \/ (A \/ B) = B )
proof
assume (Int (Cl (A \/ B))) \/ (A \/ B) = B ; ::_thesis: A c= B
then A2: A \/ B c= B by XBOOLE_1:7;
A c= A \/ B by XBOOLE_1:7;
hence A c= B by A2, XBOOLE_1:1; ::_thesis: verum
end;
thus ( A c= B implies (Int (Cl (A \/ B))) \/ (A \/ B) = B ) ::_thesis: verum
proof
assume A c= B ; ::_thesis: (Int (Cl (A \/ B))) \/ (A \/ B) = B
then A3: A \/ B = B by XBOOLE_1:12;
then Int (Cl (A \/ B)) c= B by A1, TOPS_1:def_6;
hence (Int (Cl (A \/ B))) \/ (A \/ B) = B by A3, XBOOLE_1:12; ::_thesis: verum
end;
end;
theorem :: TDLAT_2:60
for T being non empty TopSpace
for A, B being Subset of T st A is condensed holds
( (Cl (Int (A /\ B))) /\ (A /\ B) = A iff A c= B )
proof
let T be non empty TopSpace; ::_thesis: for A, B being Subset of T st A is condensed holds
( (Cl (Int (A /\ B))) /\ (A /\ B) = A iff A c= B )
let A, B be Subset of T; ::_thesis: ( A is condensed implies ( (Cl (Int (A /\ B))) /\ (A /\ B) = A iff A c= B ) )
assume A1: A is condensed ; ::_thesis: ( (Cl (Int (A /\ B))) /\ (A /\ B) = A iff A c= B )
thus ( (Cl (Int (A /\ B))) /\ (A /\ B) = A implies A c= B ) ::_thesis: ( A c= B implies (Cl (Int (A /\ B))) /\ (A /\ B) = A )
proof
assume (Cl (Int (A /\ B))) /\ (A /\ B) = A ; ::_thesis: A c= B
then A2: A c= A /\ B by XBOOLE_1:17;
A /\ B c= B by XBOOLE_1:17;
hence A c= B by A2, XBOOLE_1:1; ::_thesis: verum
end;
thus ( A c= B implies (Cl (Int (A /\ B))) /\ (A /\ B) = A ) ::_thesis: verum
proof
assume A c= B ; ::_thesis: (Cl (Int (A /\ B))) /\ (A /\ B) = A
then A3: A /\ B = A by XBOOLE_1:28;
then A c= Cl (Int (A /\ B)) by A1, TOPS_1:def_6;
hence (Cl (Int (A /\ B))) /\ (A /\ B) = A by A3, XBOOLE_1:28; ::_thesis: verum
end;
end;
theorem :: TDLAT_2:61
for T being non empty TopSpace
for A, B being Subset of T st A is closed_condensed & B is closed_condensed holds
( Int A c= Int B iff A c= B )
proof
let T be non empty TopSpace; ::_thesis: for A, B being Subset of T st A is closed_condensed & B is closed_condensed holds
( Int A c= Int B iff A c= B )
let A, B be Subset of T; ::_thesis: ( A is closed_condensed & B is closed_condensed implies ( Int A c= Int B iff A c= B ) )
assume that
A1: A is closed_condensed and
A2: B is closed_condensed ; ::_thesis: ( Int A c= Int B iff A c= B )
thus ( Int A c= Int B implies A c= B ) ::_thesis: ( A c= B implies Int A c= Int B )
proof
assume Int A c= Int B ; ::_thesis: A c= B
then A3: Cl (Int A) c= Cl (Int B) by PRE_TOPC:19;
Cl (Int A) = A by A1, TOPS_1:def_7;
hence A c= B by A2, A3, TOPS_1:def_7; ::_thesis: verum
end;
thus ( A c= B implies Int A c= Int B ) by TOPS_1:19; ::_thesis: verum
end;
theorem :: TDLAT_2:62
for T being non empty TopSpace
for A, B being Subset of T st A is open_condensed & B is open_condensed holds
( Cl A c= Cl B iff A c= B )
proof
let T be non empty TopSpace; ::_thesis: for A, B being Subset of T st A is open_condensed & B is open_condensed holds
( Cl A c= Cl B iff A c= B )
let A, B be Subset of T; ::_thesis: ( A is open_condensed & B is open_condensed implies ( Cl A c= Cl B iff A c= B ) )
assume that
A1: A is open_condensed and
A2: B is open_condensed ; ::_thesis: ( Cl A c= Cl B iff A c= B )
thus ( Cl A c= Cl B implies A c= B ) ::_thesis: ( A c= B implies Cl A c= Cl B )
proof
assume Cl A c= Cl B ; ::_thesis: A c= B
then A3: Int (Cl A) c= Int (Cl B) by TOPS_1:19;
Int (Cl A) = A by A1, TOPS_1:def_8;
hence A c= B by A2, A3, TOPS_1:def_8; ::_thesis: verum
end;
thus ( A c= B implies Cl A c= Cl B ) by PRE_TOPC:19; ::_thesis: verum
end;
theorem :: TDLAT_2:63
for T being non empty TopSpace
for A, B being Subset of T st A is closed_condensed & A c= B holds
Cl (Int (A /\ B)) = A
proof
let T be non empty TopSpace; ::_thesis: for A, B being Subset of T st A is closed_condensed & A c= B holds
Cl (Int (A /\ B)) = A
let A, B be Subset of T; ::_thesis: ( A is closed_condensed & A c= B implies Cl (Int (A /\ B)) = A )
assume A1: A is closed_condensed ; ::_thesis: ( not A c= B or Cl (Int (A /\ B)) = A )
assume A c= B ; ::_thesis: Cl (Int (A /\ B)) = A
then A /\ B = A by XBOOLE_1:28;
hence Cl (Int (A /\ B)) = A by A1, TOPS_1:def_7; ::_thesis: verum
end;
theorem Th64: :: TDLAT_2:64
for T being non empty TopSpace
for A, B being Subset of T st B is open_condensed & A c= B holds
Int (Cl (A \/ B)) = B
proof
let T be non empty TopSpace; ::_thesis: for A, B being Subset of T st B is open_condensed & A c= B holds
Int (Cl (A \/ B)) = B
let A, B be Subset of T; ::_thesis: ( B is open_condensed & A c= B implies Int (Cl (A \/ B)) = B )
assume A1: B is open_condensed ; ::_thesis: ( not A c= B or Int (Cl (A \/ B)) = B )
assume A c= B ; ::_thesis: Int (Cl (A \/ B)) = B
then A \/ B = B by XBOOLE_1:12;
hence Int (Cl (A \/ B)) = B by A1, TOPS_1:def_8; ::_thesis: verum
end;
definition
let T be non empty TopSpace;
let IT be Subset-Family of T;
attrIT is domains-family means :Def2: :: TDLAT_2:def 2
for A being Subset of T st A in IT holds
A is condensed ;
end;
:: deftheorem Def2 defines domains-family TDLAT_2:def_2_:_
for T being non empty TopSpace
for IT being Subset-Family of T holds
( IT is domains-family iff for A being Subset of T st A in IT holds
A is condensed );
theorem Th65: :: TDLAT_2:65
for T being non empty TopSpace
for F being Subset-Family of T holds
( F c= Domains_of T iff F is domains-family )
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds
( F c= Domains_of T iff F is domains-family )
let F be Subset-Family of T; ::_thesis: ( F c= Domains_of T iff F is domains-family )
thus ( F c= Domains_of T implies F is domains-family ) ::_thesis: ( F is domains-family implies F c= Domains_of T )
proof
assume A1: F c= Domains_of T ; ::_thesis: F is domains-family
now__::_thesis:_for_A_being_Subset_of_T_st_A_in_F_holds_
A_is_condensed
let A be Subset of T; ::_thesis: ( A in F implies A is condensed )
assume A in F ; ::_thesis: A is condensed
then A in Domains_of T by A1;
then A in { P where P is Subset of T : P is condensed } by TDLAT_1:def_1;
then ex Q being Subset of T st
( Q = A & Q is condensed ) ;
hence A is condensed ; ::_thesis: verum
end;
hence F is domains-family by Def2; ::_thesis: verum
end;
thus ( F is domains-family implies F c= Domains_of T ) ::_thesis: verum
proof
assume A2: F is domains-family ; ::_thesis: F c= Domains_of T
for X being set st X in F holds
X in Domains_of T
proof
let X be set ; ::_thesis: ( X in F implies X in Domains_of T )
assume A3: X in F ; ::_thesis: X in Domains_of T
then reconsider X0 = X as Subset of T ;
X0 is condensed by A2, A3, Def2;
then X0 in { P where P is Subset of T : P is condensed } ;
hence X in Domains_of T by TDLAT_1:def_1; ::_thesis: verum
end;
hence F c= Domains_of T by TARSKI:def_3; ::_thesis: verum
end;
end;
theorem Th66: :: TDLAT_2:66
for T being non empty TopSpace
for F being Subset-Family of T st F is domains-family holds
( union F c= Cl (Int (union F)) & Cl (union F) = Cl (Int (Cl (union F))) )
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st F is domains-family holds
( union F c= Cl (Int (union F)) & Cl (union F) = Cl (Int (Cl (union F))) )
let F be Subset-Family of T; ::_thesis: ( F is domains-family implies ( union F c= Cl (Int (union F)) & Cl (union F) = Cl (Int (Cl (union F))) ) )
assume A1: F is domains-family ; ::_thesis: ( union F c= Cl (Int (union F)) & Cl (union F) = Cl (Int (Cl (union F))) )
now__::_thesis:_for_A_being_Subset_of_T_st_A_in_F_holds_
A_c=_Cl_(Int_A)
let A be Subset of T; ::_thesis: ( A in F implies A c= Cl (Int A) )
reconsider B = A as Subset of T ;
assume A in F ; ::_thesis: A c= Cl (Int A)
then B is condensed by A1, Def2;
hence A c= Cl (Int A) by TOPS_1:def_6; ::_thesis: verum
end;
hence ( union F c= Cl (Int (union F)) & Cl (union F) = Cl (Int (Cl (union F))) ) by Th57; ::_thesis: verum
end;
theorem Th67: :: TDLAT_2:67
for T being non empty TopSpace
for F being Subset-Family of T st F is domains-family holds
( Int (Cl (meet F)) c= meet F & Int (Cl (Int (meet F))) = Int (meet F) )
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st F is domains-family holds
( Int (Cl (meet F)) c= meet F & Int (Cl (Int (meet F))) = Int (meet F) )
let F be Subset-Family of T; ::_thesis: ( F is domains-family implies ( Int (Cl (meet F)) c= meet F & Int (Cl (Int (meet F))) = Int (meet F) ) )
assume A1: F is domains-family ; ::_thesis: ( Int (Cl (meet F)) c= meet F & Int (Cl (Int (meet F))) = Int (meet F) )
now__::_thesis:_for_A_being_Subset_of_T_st_A_in_F_holds_
Int_(Cl_A)_c=_A
let A be Subset of T; ::_thesis: ( A in F implies Int (Cl A) c= A )
reconsider B = A as Subset of T ;
assume A in F ; ::_thesis: Int (Cl A) c= A
then B is condensed by A1, Def2;
hence Int (Cl A) c= A by TOPS_1:def_6; ::_thesis: verum
end;
hence ( Int (Cl (meet F)) c= meet F & Int (Cl (Int (meet F))) = Int (meet F) ) by Th58; ::_thesis: verum
end;
theorem Th68: :: TDLAT_2:68
for T being non empty TopSpace
for F being Subset-Family of T st F is domains-family holds
(union F) \/ (Int (Cl (union F))) is condensed
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st F is domains-family holds
(union F) \/ (Int (Cl (union F))) is condensed
let F be Subset-Family of T; ::_thesis: ( F is domains-family implies (union F) \/ (Int (Cl (union F))) is condensed )
A1: Cl (Int (Cl (union F))) c= Cl (Cl (union F)) by PRE_TOPC:19, TOPS_1:16;
assume F is domains-family ; ::_thesis: (union F) \/ (Int (Cl (union F))) is condensed
then union F c= Cl (Int (union F)) by Th66;
then A2: (union F) \/ (Int (Cl (union F))) c= Cl (Int ((union F) \/ (Int (Cl (union F))))) by Th5;
Int (Cl ((union F) \/ (Int (Cl (union F))))) = Int ((Cl (union F)) \/ (Cl (Int (Cl (union F))))) by PRE_TOPC:20
.= Int (Cl (union F)) by A1, XBOOLE_1:12 ;
then Int (Cl ((union F) \/ (Int (Cl (union F))))) c= (union F) \/ (Int (Cl (union F))) by XBOOLE_1:7;
hence (union F) \/ (Int (Cl (union F))) is condensed by A2, TOPS_1:def_6; ::_thesis: verum
end;
theorem Th69: :: TDLAT_2:69
for T being non empty TopSpace
for F being Subset-Family of T holds
( ( for B being Subset of T st B in F holds
B c= (union F) \/ (Int (Cl (union F))) ) & ( for A being Subset of T st A is condensed & ( for B being Subset of T st B in F holds
B c= A ) holds
(union F) \/ (Int (Cl (union F))) c= A ) )
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds
( ( for B being Subset of T st B in F holds
B c= (union F) \/ (Int (Cl (union F))) ) & ( for A being Subset of T st A is condensed & ( for B being Subset of T st B in F holds
B c= A ) holds
(union F) \/ (Int (Cl (union F))) c= A ) )
let F be Subset-Family of T; ::_thesis: ( ( for B being Subset of T st B in F holds
B c= (union F) \/ (Int (Cl (union F))) ) & ( for A being Subset of T st A is condensed & ( for B being Subset of T st B in F holds
B c= A ) holds
(union F) \/ (Int (Cl (union F))) c= A ) )
thus for B being Subset of T st B in F holds
B c= (union F) \/ (Int (Cl (union F))) ::_thesis: for A being Subset of T st A is condensed & ( for B being Subset of T st B in F holds
B c= A ) holds
(union F) \/ (Int (Cl (union F))) c= A
proof
let B be Subset of T; ::_thesis: ( B in F implies B c= (union F) \/ (Int (Cl (union F))) )
assume B in F ; ::_thesis: B c= (union F) \/ (Int (Cl (union F)))
then A1: B c= union F by ZFMISC_1:74;
union F c= (union F) \/ (Int (Cl (union F))) by XBOOLE_1:7;
hence B c= (union F) \/ (Int (Cl (union F))) by A1, XBOOLE_1:1; ::_thesis: verum
end;
thus for A being Subset of T st A is condensed & ( for B being Subset of T st B in F holds
B c= A ) holds
(union F) \/ (Int (Cl (union F))) c= A ::_thesis: verum
proof
let A be Subset of T; ::_thesis: ( A is condensed & ( for B being Subset of T st B in F holds
B c= A ) implies (union F) \/ (Int (Cl (union F))) c= A )
assume A is condensed ; ::_thesis: ( ex B being Subset of T st
( B in F & not B c= A ) or (union F) \/ (Int (Cl (union F))) c= A )
then A2: Int (Cl A) c= A by TOPS_1:def_6;
assume for B being Subset of T st B in F holds
B c= A ; ::_thesis: (union F) \/ (Int (Cl (union F))) c= A
then for P being set st P in F holds
P c= A ;
then A3: union F c= A by ZFMISC_1:76;
then Cl (union F) c= Cl A by PRE_TOPC:19;
then Int (Cl (union F)) c= Int (Cl A) by TOPS_1:19;
then Int (Cl (union F)) c= A by A2, XBOOLE_1:1;
hence (union F) \/ (Int (Cl (union F))) c= A by A3, XBOOLE_1:8; ::_thesis: verum
end;
end;
theorem Th70: :: TDLAT_2:70
for T being non empty TopSpace
for F being Subset-Family of T st F is domains-family holds
(meet F) /\ (Cl (Int (meet F))) is condensed
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st F is domains-family holds
(meet F) /\ (Cl (Int (meet F))) is condensed
let F be Subset-Family of T; ::_thesis: ( F is domains-family implies (meet F) /\ (Cl (Int (meet F))) is condensed )
A1: Int (Int (meet F)) c= Int (Cl (Int (meet F))) by PRE_TOPC:18, TOPS_1:19;
assume F is domains-family ; ::_thesis: (meet F) /\ (Cl (Int (meet F))) is condensed
then Int (Cl (meet F)) c= meet F by Th67;
then A2: Int (Cl ((meet F) /\ (Cl (Int (meet F))))) c= (meet F) /\ (Cl (Int (meet F))) by Th6;
Cl (Int ((meet F) /\ (Cl (Int (meet F))))) = Cl ((Int (meet F)) /\ (Int (Cl (Int (meet F))))) by TOPS_1:17
.= Cl (Int (meet F)) by A1, XBOOLE_1:28 ;
then (meet F) /\ (Cl (Int (meet F))) c= Cl (Int ((meet F) /\ (Cl (Int (meet F))))) by XBOOLE_1:17;
hence (meet F) /\ (Cl (Int (meet F))) is condensed by A2, TOPS_1:def_6; ::_thesis: verum
end;
theorem Th71: :: TDLAT_2:71
for T being non empty TopSpace
for F being Subset-Family of T holds
( ( for B being Subset of T st B in F holds
(meet F) /\ (Cl (Int (meet F))) c= B ) & ( F = {} or for A being Subset of T st A is condensed & ( for B being Subset of T st B in F holds
A c= B ) holds
A c= (meet F) /\ (Cl (Int (meet F))) ) )
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds
( ( for B being Subset of T st B in F holds
(meet F) /\ (Cl (Int (meet F))) c= B ) & ( F = {} or for A being Subset of T st A is condensed & ( for B being Subset of T st B in F holds
A c= B ) holds
A c= (meet F) /\ (Cl (Int (meet F))) ) )
let F be Subset-Family of T; ::_thesis: ( ( for B being Subset of T st B in F holds
(meet F) /\ (Cl (Int (meet F))) c= B ) & ( F = {} or for A being Subset of T st A is condensed & ( for B being Subset of T st B in F holds
A c= B ) holds
A c= (meet F) /\ (Cl (Int (meet F))) ) )
thus for B being Subset of T st B in F holds
(meet F) /\ (Cl (Int (meet F))) c= B ::_thesis: ( F = {} or for A being Subset of T st A is condensed & ( for B being Subset of T st B in F holds
A c= B ) holds
A c= (meet F) /\ (Cl (Int (meet F))) )
proof
let B be Subset of T; ::_thesis: ( B in F implies (meet F) /\ (Cl (Int (meet F))) c= B )
assume B in F ; ::_thesis: (meet F) /\ (Cl (Int (meet F))) c= B
then A1: meet F c= B by SETFAM_1:3;
(meet F) /\ (Cl (Int (meet F))) c= meet F by XBOOLE_1:17;
hence (meet F) /\ (Cl (Int (meet F))) c= B by A1, XBOOLE_1:1; ::_thesis: verum
end;
thus ( F = {} or for A being Subset of T st A is condensed & ( for B being Subset of T st B in F holds
A c= B ) holds
A c= (meet F) /\ (Cl (Int (meet F))) ) ::_thesis: verum
proof
assume A2: F <> {} ; ::_thesis: for A being Subset of T st A is condensed & ( for B being Subset of T st B in F holds
A c= B ) holds
A c= (meet F) /\ (Cl (Int (meet F)))
let A be Subset of T; ::_thesis: ( A is condensed & ( for B being Subset of T st B in F holds
A c= B ) implies A c= (meet F) /\ (Cl (Int (meet F))) )
assume A is condensed ; ::_thesis: ( ex B being Subset of T st
( B in F & not A c= B ) or A c= (meet F) /\ (Cl (Int (meet F))) )
then A3: A c= Cl (Int A) by TOPS_1:def_6;
assume for B being Subset of T st B in F holds
A c= B ; ::_thesis: A c= (meet F) /\ (Cl (Int (meet F)))
then for P being set st P in F holds
A c= P ;
then A4: A c= meet F by A2, SETFAM_1:5;
then Int A c= Int (meet F) by TOPS_1:19;
then Cl (Int A) c= Cl (Int (meet F)) by PRE_TOPC:19;
then A c= Cl (Int (meet F)) by A3, XBOOLE_1:1;
hence A c= (meet F) /\ (Cl (Int (meet F))) by A4, XBOOLE_1:19; ::_thesis: verum
end;
end;
definition
let T be non empty TopSpace;
let IT be Subset-Family of T;
attrIT is closed-domains-family means :Def3: :: TDLAT_2:def 3
for A being Subset of T st A in IT holds
A is closed_condensed ;
end;
:: deftheorem Def3 defines closed-domains-family TDLAT_2:def_3_:_
for T being non empty TopSpace
for IT being Subset-Family of T holds
( IT is closed-domains-family iff for A being Subset of T st A in IT holds
A is closed_condensed );
theorem Th72: :: TDLAT_2:72
for T being non empty TopSpace
for F being Subset-Family of T holds
( F c= Closed_Domains_of T iff F is closed-domains-family )
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds
( F c= Closed_Domains_of T iff F is closed-domains-family )
let F be Subset-Family of T; ::_thesis: ( F c= Closed_Domains_of T iff F is closed-domains-family )
thus ( F c= Closed_Domains_of T implies F is closed-domains-family ) ::_thesis: ( F is closed-domains-family implies F c= Closed_Domains_of T )
proof
assume A1: F c= Closed_Domains_of T ; ::_thesis: F is closed-domains-family
now__::_thesis:_for_A_being_Subset_of_T_st_A_in_F_holds_
A_is_closed_condensed
let A be Subset of T; ::_thesis: ( A in F implies A is closed_condensed )
assume A in F ; ::_thesis: A is closed_condensed
then A in Closed_Domains_of T by A1;
then A in { P where P is Subset of T : P is closed_condensed } by TDLAT_1:def_5;
then ex Q being Subset of T st
( Q = A & Q is closed_condensed ) ;
hence A is closed_condensed ; ::_thesis: verum
end;
hence F is closed-domains-family by Def3; ::_thesis: verum
end;
thus ( F is closed-domains-family implies F c= Closed_Domains_of T ) ::_thesis: verum
proof
assume A2: F is closed-domains-family ; ::_thesis: F c= Closed_Domains_of T
for X being set st X in F holds
X in Closed_Domains_of T
proof
let X be set ; ::_thesis: ( X in F implies X in Closed_Domains_of T )
assume A3: X in F ; ::_thesis: X in Closed_Domains_of T
then reconsider X0 = X as Subset of T ;
X0 is closed_condensed by A2, A3, Def3;
then X0 in { P where P is Subset of T : P is closed_condensed } ;
hence X in Closed_Domains_of T by TDLAT_1:def_5; ::_thesis: verum
end;
hence F c= Closed_Domains_of T by TARSKI:def_3; ::_thesis: verum
end;
end;
theorem Th73: :: TDLAT_2:73
for T being non empty TopSpace
for F being Subset-Family of T st F is closed-domains-family holds
F is domains-family
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st F is closed-domains-family holds
F is domains-family
let F be Subset-Family of T; ::_thesis: ( F is closed-domains-family implies F is domains-family )
thus ( F is closed-domains-family implies F is domains-family ) ::_thesis: verum
proof
assume F is closed-domains-family ; ::_thesis: F is domains-family
then A1: F c= Closed_Domains_of T by Th72;
Closed_Domains_of T c= Domains_of T by TDLAT_1:31;
then F c= Domains_of T by A1, XBOOLE_1:1;
hence F is domains-family by Th65; ::_thesis: verum
end;
end;
theorem Th74: :: TDLAT_2:74
for T being non empty TopSpace
for F being Subset-Family of T st F is closed-domains-family holds
F is closed
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st F is closed-domains-family holds
F is closed
let F be Subset-Family of T; ::_thesis: ( F is closed-domains-family implies F is closed )
assume A1: F is closed-domains-family ; ::_thesis: F is closed
for A being Subset of T st A in F holds
A is closed
proof
let A be Subset of T; ::_thesis: ( A in F implies A is closed )
assume A in F ; ::_thesis: A is closed
then A is closed_condensed by A1, Def3;
hence A is closed by TOPS_1:66; ::_thesis: verum
end;
hence F is closed by TOPS_2:def_2; ::_thesis: verum
end;
theorem :: TDLAT_2:75
for T being non empty TopSpace
for F being Subset-Family of T st F is domains-family holds
Cl F is closed-domains-family
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st F is domains-family holds
Cl F is closed-domains-family
let F be Subset-Family of T; ::_thesis: ( F is domains-family implies Cl F is closed-domains-family )
assume A1: F is domains-family ; ::_thesis: Cl F is closed-domains-family
for A being Subset of T st A in Cl F holds
A is closed_condensed
proof
let A be Subset of T; ::_thesis: ( A in Cl F implies A is closed_condensed )
assume A in Cl F ; ::_thesis: A is closed_condensed
then consider P being Subset of T such that
A2: A = Cl P and
A3: P in F by PCOMPS_1:def_2;
reconsider P = P as Subset of T ;
P is condensed by A1, A3, Def2;
hence A is closed_condensed by A2, TDLAT_1:24; ::_thesis: verum
end;
hence Cl F is closed-domains-family by Def3; ::_thesis: verum
end;
theorem Th76: :: TDLAT_2:76
for T being non empty TopSpace
for F being Subset-Family of T st F is closed-domains-family holds
( Cl (union F) is closed_condensed & Cl (Int (meet F)) is closed_condensed )
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st F is closed-domains-family holds
( Cl (union F) is closed_condensed & Cl (Int (meet F)) is closed_condensed )
let F be Subset-Family of T; ::_thesis: ( F is closed-domains-family implies ( Cl (union F) is closed_condensed & Cl (Int (meet F)) is closed_condensed ) )
assume F is closed-domains-family ; ::_thesis: ( Cl (union F) is closed_condensed & Cl (Int (meet F)) is closed_condensed )
then F is domains-family by Th73;
then Cl (union F) = Cl (Int (Cl (union F))) by Th66;
hence Cl (union F) is closed_condensed by TOPS_1:def_7; ::_thesis: Cl (Int (meet F)) is closed_condensed
thus Cl (Int (meet F)) is closed_condensed by TDLAT_1:22; ::_thesis: verum
end;
theorem Th77: :: TDLAT_2:77
for T being non empty TopSpace
for F being Subset-Family of T holds
( ( for B being Subset of T st B in F holds
B c= Cl (union F) ) & ( for A being Subset of T st A is closed_condensed & ( for B being Subset of T st B in F holds
B c= A ) holds
Cl (union F) c= A ) )
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds
( ( for B being Subset of T st B in F holds
B c= Cl (union F) ) & ( for A being Subset of T st A is closed_condensed & ( for B being Subset of T st B in F holds
B c= A ) holds
Cl (union F) c= A ) )
let F be Subset-Family of T; ::_thesis: ( ( for B being Subset of T st B in F holds
B c= Cl (union F) ) & ( for A being Subset of T st A is closed_condensed & ( for B being Subset of T st B in F holds
B c= A ) holds
Cl (union F) c= A ) )
thus for B being Subset of T st B in F holds
B c= Cl (union F) ::_thesis: for A being Subset of T st A is closed_condensed & ( for B being Subset of T st B in F holds
B c= A ) holds
Cl (union F) c= A
proof
let B be Subset of T; ::_thesis: ( B in F implies B c= Cl (union F) )
assume B in F ; ::_thesis: B c= Cl (union F)
then A1: B c= union F by ZFMISC_1:74;
union F c= Cl (union F) by PRE_TOPC:18;
hence B c= Cl (union F) by A1, XBOOLE_1:1; ::_thesis: verum
end;
thus for A being Subset of T st A is closed_condensed & ( for B being Subset of T st B in F holds
B c= A ) holds
Cl (union F) c= A ::_thesis: verum
proof
let A be Subset of T; ::_thesis: ( A is closed_condensed & ( for B being Subset of T st B in F holds
B c= A ) implies Cl (union F) c= A )
reconsider A1 = A as Subset of T ;
assume A is closed_condensed ; ::_thesis: ( ex B being Subset of T st
( B in F & not B c= A ) or Cl (union F) c= A )
then A2: A1 is closed by TOPS_1:66;
assume for B being Subset of T st B in F holds
B c= A ; ::_thesis: Cl (union F) c= A
then for P being set st P in F holds
P c= A ;
then union F c= A by ZFMISC_1:76;
then Cl (union F) c= Cl A by PRE_TOPC:19;
hence Cl (union F) c= A by A2, PRE_TOPC:22; ::_thesis: verum
end;
end;
theorem Th78: :: TDLAT_2:78
for T being non empty TopSpace
for F being Subset-Family of T holds
( ( F is closed implies for B being Subset of T st B in F holds
Cl (Int (meet F)) c= B ) & ( F = {} or for A being Subset of T st A is closed_condensed & ( for B being Subset of T st B in F holds
A c= B ) holds
A c= Cl (Int (meet F)) ) )
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds
( ( F is closed implies for B being Subset of T st B in F holds
Cl (Int (meet F)) c= B ) & ( F = {} or for A being Subset of T st A is closed_condensed & ( for B being Subset of T st B in F holds
A c= B ) holds
A c= Cl (Int (meet F)) ) )
let F be Subset-Family of T; ::_thesis: ( ( F is closed implies for B being Subset of T st B in F holds
Cl (Int (meet F)) c= B ) & ( F = {} or for A being Subset of T st A is closed_condensed & ( for B being Subset of T st B in F holds
A c= B ) holds
A c= Cl (Int (meet F)) ) )
thus ( F is closed implies for B being Subset of T st B in F holds
Cl (Int (meet F)) c= B ) ::_thesis: ( F = {} or for A being Subset of T st A is closed_condensed & ( for B being Subset of T st B in F holds
A c= B ) holds
A c= Cl (Int (meet F)) )
proof
assume F is closed ; ::_thesis: for B being Subset of T st B in F holds
Cl (Int (meet F)) c= B
then meet F is closed by TOPS_2:22;
then A1: Cl (meet F) = meet F by PRE_TOPC:22;
let B be Subset of T; ::_thesis: ( B in F implies Cl (Int (meet F)) c= B )
A2: Cl (Int (meet F)) c= Cl (meet F) by PRE_TOPC:19, TOPS_1:16;
assume B in F ; ::_thesis: Cl (Int (meet F)) c= B
then meet F c= B by SETFAM_1:3;
hence Cl (Int (meet F)) c= B by A2, A1, XBOOLE_1:1; ::_thesis: verum
end;
thus ( F = {} or for A being Subset of T st A is closed_condensed & ( for B being Subset of T st B in F holds
A c= B ) holds
A c= Cl (Int (meet F)) ) ::_thesis: verum
proof
assume A3: F <> {} ; ::_thesis: for A being Subset of T st A is closed_condensed & ( for B being Subset of T st B in F holds
A c= B ) holds
A c= Cl (Int (meet F))
let A be Subset of T; ::_thesis: ( A is closed_condensed & ( for B being Subset of T st B in F holds
A c= B ) implies A c= Cl (Int (meet F)) )
assume A4: A is closed_condensed ; ::_thesis: ( ex B being Subset of T st
( B in F & not A c= B ) or A c= Cl (Int (meet F)) )
assume for B being Subset of T st B in F holds
A c= B ; ::_thesis: A c= Cl (Int (meet F))
then for P being set st P in F holds
A c= P ;
then A c= meet F by A3, SETFAM_1:5;
then A5: Int A c= Int (meet F) by TOPS_1:19;
A = Cl (Int A) by A4, TOPS_1:def_7;
hence A c= Cl (Int (meet F)) by A5, PRE_TOPC:19; ::_thesis: verum
end;
end;
definition
let T be non empty TopSpace;
let IT be Subset-Family of T;
attrIT is open-domains-family means :Def4: :: TDLAT_2:def 4
for A being Subset of T st A in IT holds
A is open_condensed ;
end;
:: deftheorem Def4 defines open-domains-family TDLAT_2:def_4_:_
for T being non empty TopSpace
for IT being Subset-Family of T holds
( IT is open-domains-family iff for A being Subset of T st A in IT holds
A is open_condensed );
theorem Th79: :: TDLAT_2:79
for T being non empty TopSpace
for F being Subset-Family of T holds
( F c= Open_Domains_of T iff F is open-domains-family )
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds
( F c= Open_Domains_of T iff F is open-domains-family )
let F be Subset-Family of T; ::_thesis: ( F c= Open_Domains_of T iff F is open-domains-family )
thus ( F c= Open_Domains_of T implies F is open-domains-family ) ::_thesis: ( F is open-domains-family implies F c= Open_Domains_of T )
proof
assume A1: F c= Open_Domains_of T ; ::_thesis: F is open-domains-family
now__::_thesis:_for_A_being_Subset_of_T_st_A_in_F_holds_
A_is_open_condensed
let A be Subset of T; ::_thesis: ( A in F implies A is open_condensed )
assume A in F ; ::_thesis: A is open_condensed
then A in Open_Domains_of T by A1;
then A in { P where P is Subset of T : P is open_condensed } by TDLAT_1:def_9;
then ex Q being Subset of T st
( Q = A & Q is open_condensed ) ;
hence A is open_condensed ; ::_thesis: verum
end;
hence F is open-domains-family by Def4; ::_thesis: verum
end;
thus ( F is open-domains-family implies F c= Open_Domains_of T ) ::_thesis: verum
proof
assume A2: F is open-domains-family ; ::_thesis: F c= Open_Domains_of T
for X being set st X in F holds
X in Open_Domains_of T
proof
let X be set ; ::_thesis: ( X in F implies X in Open_Domains_of T )
assume A3: X in F ; ::_thesis: X in Open_Domains_of T
then reconsider X0 = X as Subset of T ;
X0 is open_condensed by A2, A3, Def4;
then X0 in { P where P is Subset of T : P is open_condensed } ;
hence X in Open_Domains_of T by TDLAT_1:def_9; ::_thesis: verum
end;
hence F c= Open_Domains_of T by TARSKI:def_3; ::_thesis: verum
end;
end;
theorem Th80: :: TDLAT_2:80
for T being non empty TopSpace
for F being Subset-Family of T st F is open-domains-family holds
F is domains-family
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st F is open-domains-family holds
F is domains-family
let F be Subset-Family of T; ::_thesis: ( F is open-domains-family implies F is domains-family )
thus ( F is open-domains-family implies F is domains-family ) ::_thesis: verum
proof
assume F is open-domains-family ; ::_thesis: F is domains-family
then A1: F c= Open_Domains_of T by Th79;
Open_Domains_of T c= Domains_of T by TDLAT_1:35;
then F c= Domains_of T by A1, XBOOLE_1:1;
hence F is domains-family by Th65; ::_thesis: verum
end;
end;
theorem Th81: :: TDLAT_2:81
for T being non empty TopSpace
for F being Subset-Family of T st F is open-domains-family holds
F is open
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st F is open-domains-family holds
F is open
let F be Subset-Family of T; ::_thesis: ( F is open-domains-family implies F is open )
assume A1: F is open-domains-family ; ::_thesis: F is open
for A being Subset of T st A in F holds
A is open
proof
let A be Subset of T; ::_thesis: ( A in F implies A is open )
assume A in F ; ::_thesis: A is open
then A is open_condensed by A1, Def4;
hence A is open by TOPS_1:67; ::_thesis: verum
end;
hence F is open by TOPS_2:def_1; ::_thesis: verum
end;
theorem :: TDLAT_2:82
for T being non empty TopSpace
for F being Subset-Family of T st F is domains-family holds
Int F is open-domains-family
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st F is domains-family holds
Int F is open-domains-family
let F be Subset-Family of T; ::_thesis: ( F is domains-family implies Int F is open-domains-family )
assume A1: F is domains-family ; ::_thesis: Int F is open-domains-family
for A being Subset of T st A in Int F holds
A is open_condensed
proof
let A be Subset of T; ::_thesis: ( A in Int F implies A is open_condensed )
assume A in Int F ; ::_thesis: A is open_condensed
then consider P being Subset of T such that
A2: A = Int P and
A3: P in F by Def1;
reconsider P = P as Subset of T ;
P is condensed by A1, A3, Def2;
hence A is open_condensed by A2, TDLAT_1:25; ::_thesis: verum
end;
hence Int F is open-domains-family by Def4; ::_thesis: verum
end;
theorem Th83: :: TDLAT_2:83
for T being non empty TopSpace
for F being Subset-Family of T st F is open-domains-family holds
( Int (meet F) is open_condensed & Int (Cl (union F)) is open_condensed )
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st F is open-domains-family holds
( Int (meet F) is open_condensed & Int (Cl (union F)) is open_condensed )
let F be Subset-Family of T; ::_thesis: ( F is open-domains-family implies ( Int (meet F) is open_condensed & Int (Cl (union F)) is open_condensed ) )
assume F is open-domains-family ; ::_thesis: ( Int (meet F) is open_condensed & Int (Cl (union F)) is open_condensed )
then F is domains-family by Th80;
then Int (Cl (Int (meet F))) = Int (meet F) by Th67;
hence Int (meet F) is open_condensed by TOPS_1:def_8; ::_thesis: Int (Cl (union F)) is open_condensed
thus Int (Cl (union F)) is open_condensed by TDLAT_1:23; ::_thesis: verum
end;
theorem Th84: :: TDLAT_2:84
for T being non empty TopSpace
for F being Subset-Family of T holds
( ( F is open implies for B being Subset of T st B in F holds
B c= Int (Cl (union F)) ) & ( for A being Subset of T st A is open_condensed & ( for B being Subset of T st B in F holds
B c= A ) holds
Int (Cl (union F)) c= A ) )
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds
( ( F is open implies for B being Subset of T st B in F holds
B c= Int (Cl (union F)) ) & ( for A being Subset of T st A is open_condensed & ( for B being Subset of T st B in F holds
B c= A ) holds
Int (Cl (union F)) c= A ) )
let F be Subset-Family of T; ::_thesis: ( ( F is open implies for B being Subset of T st B in F holds
B c= Int (Cl (union F)) ) & ( for A being Subset of T st A is open_condensed & ( for B being Subset of T st B in F holds
B c= A ) holds
Int (Cl (union F)) c= A ) )
thus ( F is open implies for B being Subset of T st B in F holds
B c= Int (Cl (union F)) ) ::_thesis: for A being Subset of T st A is open_condensed & ( for B being Subset of T st B in F holds
B c= A ) holds
Int (Cl (union F)) c= A
proof
assume F is open ; ::_thesis: for B being Subset of T st B in F holds
B c= Int (Cl (union F))
then union F is open by TOPS_2:19;
then A1: Int (union F) = union F by TOPS_1:23;
let B be Subset of T; ::_thesis: ( B in F implies B c= Int (Cl (union F)) )
A2: Int (union F) c= Int (Cl (union F)) by PRE_TOPC:18, TOPS_1:19;
assume B in F ; ::_thesis: B c= Int (Cl (union F))
then B c= union F by ZFMISC_1:74;
hence B c= Int (Cl (union F)) by A2, A1, XBOOLE_1:1; ::_thesis: verum
end;
thus for A being Subset of T st A is open_condensed & ( for B being Subset of T st B in F holds
B c= A ) holds
Int (Cl (union F)) c= A ::_thesis: verum
proof
let A be Subset of T; ::_thesis: ( A is open_condensed & ( for B being Subset of T st B in F holds
B c= A ) implies Int (Cl (union F)) c= A )
assume A is open_condensed ; ::_thesis: ( ex B being Subset of T st
( B in F & not B c= A ) or Int (Cl (union F)) c= A )
then A3: A = Int (Cl A) by TOPS_1:def_8;
assume for B being Subset of T st B in F holds
B c= A ; ::_thesis: Int (Cl (union F)) c= A
then for P being set st P in F holds
P c= A ;
then union F c= A by ZFMISC_1:76;
then Cl (union F) c= Cl A by PRE_TOPC:19;
hence Int (Cl (union F)) c= A by A3, TOPS_1:19; ::_thesis: verum
end;
end;
theorem Th85: :: TDLAT_2:85
for T being non empty TopSpace
for F being Subset-Family of T holds
( ( for B being Subset of T st B in F holds
Int (meet F) c= B ) & ( F = {} or for A being Subset of T st A is open_condensed & ( for B being Subset of T st B in F holds
A c= B ) holds
A c= Int (meet F) ) )
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds
( ( for B being Subset of T st B in F holds
Int (meet F) c= B ) & ( F = {} or for A being Subset of T st A is open_condensed & ( for B being Subset of T st B in F holds
A c= B ) holds
A c= Int (meet F) ) )
let F be Subset-Family of T; ::_thesis: ( ( for B being Subset of T st B in F holds
Int (meet F) c= B ) & ( F = {} or for A being Subset of T st A is open_condensed & ( for B being Subset of T st B in F holds
A c= B ) holds
A c= Int (meet F) ) )
thus for B being Subset of T st B in F holds
Int (meet F) c= B ::_thesis: ( F = {} or for A being Subset of T st A is open_condensed & ( for B being Subset of T st B in F holds
A c= B ) holds
A c= Int (meet F) )
proof
let B be Subset of T; ::_thesis: ( B in F implies Int (meet F) c= B )
assume B in F ; ::_thesis: Int (meet F) c= B
then A1: meet F c= B by SETFAM_1:3;
Int (meet F) c= meet F by TOPS_1:16;
hence Int (meet F) c= B by A1, XBOOLE_1:1; ::_thesis: verum
end;
thus ( F = {} or for A being Subset of T st A is open_condensed & ( for B being Subset of T st B in F holds
A c= B ) holds
A c= Int (meet F) ) ::_thesis: verum
proof
assume A2: F <> {} ; ::_thesis: for A being Subset of T st A is open_condensed & ( for B being Subset of T st B in F holds
A c= B ) holds
A c= Int (meet F)
let A be Subset of T; ::_thesis: ( A is open_condensed & ( for B being Subset of T st B in F holds
A c= B ) implies A c= Int (meet F) )
assume A3: A is open_condensed ; ::_thesis: ( ex B being Subset of T st
( B in F & not A c= B ) or A c= Int (meet F) )
assume for B being Subset of T st B in F holds
A c= B ; ::_thesis: A c= Int (meet F)
then for P being set st P in F holds
A c= P ;
then A4: A c= meet F by A2, SETFAM_1:5;
A is open by A3, TOPS_1:67;
then Int A = A by TOPS_1:23;
hence A c= Int (meet F) by A4, TOPS_1:19; ::_thesis: verum
end;
end;
begin
theorem Th86: :: TDLAT_2:86
for T being non empty TopSpace holds the carrier of (Domains_Lattice T) = Domains_of T
proof
let T be non empty TopSpace; ::_thesis: the carrier of (Domains_Lattice T) = Domains_of T
Domains_Lattice T = LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #) by TDLAT_1:def_4;
hence the carrier of (Domains_Lattice T) = Domains_of T ; ::_thesis: verum
end;
theorem Th87: :: TDLAT_2:87
for T being non empty TopSpace
for a, b being Element of (Domains_Lattice T)
for A, B being Element of Domains_of T st a = A & b = B holds
( a "\/" b = (Int (Cl (A \/ B))) \/ (A \/ B) & a "/\" b = (Cl (Int (A /\ B))) /\ (A /\ B) )
proof
let T be non empty TopSpace; ::_thesis: for a, b being Element of (Domains_Lattice T)
for A, B being Element of Domains_of T st a = A & b = B holds
( a "\/" b = (Int (Cl (A \/ B))) \/ (A \/ B) & a "/\" b = (Cl (Int (A /\ B))) /\ (A /\ B) )
let a, b be Element of (Domains_Lattice T); ::_thesis: for A, B being Element of Domains_of T st a = A & b = B holds
( a "\/" b = (Int (Cl (A \/ B))) \/ (A \/ B) & a "/\" b = (Cl (Int (A /\ B))) /\ (A /\ B) )
let A, B be Element of Domains_of T; ::_thesis: ( a = A & b = B implies ( a "\/" b = (Int (Cl (A \/ B))) \/ (A \/ B) & a "/\" b = (Cl (Int (A /\ B))) /\ (A /\ B) ) )
assume that
A1: a = A and
A2: b = B ; ::_thesis: ( a "\/" b = (Int (Cl (A \/ B))) \/ (A \/ B) & a "/\" b = (Cl (Int (A /\ B))) /\ (A /\ B) )
A3: Domains_Lattice T = LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #) by TDLAT_1:def_4;
hence a "\/" b = (D-Union T) . (A,B) by A1, A2, LATTICES:def_1
.= (Int (Cl (A \/ B))) \/ (A \/ B) by TDLAT_1:def_2 ;
::_thesis: a "/\" b = (Cl (Int (A /\ B))) /\ (A /\ B)
thus a "/\" b = (D-Meet T) . (A,B) by A3, A1, A2, LATTICES:def_2
.= (Cl (Int (A /\ B))) /\ (A /\ B) by TDLAT_1:def_3 ; ::_thesis: verum
end;
theorem :: TDLAT_2:88
for T being non empty TopSpace holds
( Bottom (Domains_Lattice T) = {} T & Top (Domains_Lattice T) = [#] T )
proof
let T be non empty TopSpace; ::_thesis: ( Bottom (Domains_Lattice T) = {} T & Top (Domains_Lattice T) = [#] T )
thus Bottom (Domains_Lattice T) = {} T ::_thesis: Top (Domains_Lattice T) = [#] T
proof
{} T is condensed by TDLAT_1:14;
then A1: {} T in { A where A is Subset of T : A is condensed } ;
then reconsider E = {} T as Element of Domains_of T by TDLAT_1:def_1;
{} T in Domains_of T by A1, TDLAT_1:def_1;
then reconsider e = {} T as Element of (Domains_Lattice T) by Th86;
for a being Element of (Domains_Lattice T) holds e "\/" a = a
proof
let a be Element of (Domains_Lattice T); ::_thesis: e "\/" a = a
reconsider A = a as Element of Domains_of T by Th86;
A in Domains_of T ;
then A in { C where C is Subset of T : C is condensed } by TDLAT_1:def_1;
then ex D being Subset of T st
( D = A & D is condensed ) ;
then A2: Int (Cl A) c= A by TOPS_1:def_6;
thus e "\/" a = (Int (Cl (E \/ A))) \/ (E \/ A) by Th87
.= a by A2, XBOOLE_1:12 ; ::_thesis: verum
end;
hence Bottom (Domains_Lattice T) = {} T by LATTICE2:14; ::_thesis: verum
end;
thus Top (Domains_Lattice T) = [#] T ::_thesis: verum
proof
[#] T is condensed by TDLAT_1:15;
then A3: [#] T in { A where A is Subset of T : A is condensed } ;
then reconsider E = [#] T as Element of Domains_of T by TDLAT_1:def_1;
[#] T in Domains_of T by A3, TDLAT_1:def_1;
then reconsider e = [#] T as Element of (Domains_Lattice T) by Th86;
for a being Element of (Domains_Lattice T) holds e "/\" a = a
proof
let a be Element of (Domains_Lattice T); ::_thesis: e "/\" a = a
reconsider A = a as Element of Domains_of T by Th86;
A in Domains_of T ;
then A in { C where C is Subset of T : C is condensed } by TDLAT_1:def_1;
then ex D being Subset of T st
( D = A & D is condensed ) ;
then A4: A c= Cl (Int A) by TOPS_1:def_6;
thus e "/\" a = (Cl (Int (E /\ A))) /\ (E /\ A) by Th87
.= (Cl (Int A)) /\ (([#] T) /\ A) by XBOOLE_1:28
.= (Cl (Int A)) /\ A by XBOOLE_1:28
.= a by A4, XBOOLE_1:28 ; ::_thesis: verum
end;
hence Top (Domains_Lattice T) = [#] T by LATTICE2:16; ::_thesis: verum
end;
end;
theorem Th89: :: TDLAT_2:89
for T being non empty TopSpace
for a, b being Element of (Domains_Lattice T)
for A, B being Element of Domains_of T st a = A & b = B holds
( a [= b iff A c= B )
proof
let T be non empty TopSpace; ::_thesis: for a, b being Element of (Domains_Lattice T)
for A, B being Element of Domains_of T st a = A & b = B holds
( a [= b iff A c= B )
let a, b be Element of (Domains_Lattice T); ::_thesis: for A, B being Element of Domains_of T st a = A & b = B holds
( a [= b iff A c= B )
let A, B be Element of Domains_of T; ::_thesis: ( a = A & b = B implies ( a [= b iff A c= B ) )
assume that
A1: a = A and
A2: b = B ; ::_thesis: ( a [= b iff A c= B )
B in Domains_of T ;
then B in { C where C is Subset of T : C is condensed } by TDLAT_1:def_1;
then A3: ex Q being Subset of T st
( Q = B & Q is condensed ) ;
thus ( a [= b implies A c= B ) ::_thesis: ( A c= B implies a [= b )
proof
assume a [= b ; ::_thesis: A c= B
then a "\/" b = b by LATTICES:def_3;
then (Int (Cl (A \/ B))) \/ (A \/ B) = B by A1, A2, Th87;
hence A c= B by A3, Th59; ::_thesis: verum
end;
assume A c= B ; ::_thesis: a [= b
then (Int (Cl (A \/ B))) \/ (A \/ B) = B by A3, Th59;
then a "\/" b = b by A1, A2, Th87;
hence a [= b by LATTICES:def_3; ::_thesis: verum
end;
theorem Th90: :: TDLAT_2:90
for T being non empty TopSpace
for X being Subset of (Domains_Lattice T) ex a being Element of (Domains_Lattice T) st
( X is_less_than a & ( for b being Element of (Domains_Lattice T) st X is_less_than b holds
a [= b ) )
proof
let T be non empty TopSpace; ::_thesis: for X being Subset of (Domains_Lattice T) ex a being Element of (Domains_Lattice T) st
( X is_less_than a & ( for b being Element of (Domains_Lattice T) st X is_less_than b holds
a [= b ) )
let X be Subset of (Domains_Lattice T); ::_thesis: ex a being Element of (Domains_Lattice T) st
( X is_less_than a & ( for b being Element of (Domains_Lattice T) st X is_less_than b holds
a [= b ) )
X c= the carrier of (Domains_Lattice T) ;
then A1: X c= Domains_of T by Th86;
then reconsider F = X as Subset-Family of T by TOPS_2:2;
set A = (union F) \/ (Int (Cl (union F)));
A2: F is domains-family by A1, Th65;
then (union F) \/ (Int (Cl (union F))) is condensed by Th68;
then (union F) \/ (Int (Cl (union F))) in { C where C is Subset of T : C is condensed } ;
then A3: (union F) \/ (Int (Cl (union F))) in Domains_of T by TDLAT_1:def_1;
then reconsider a = (union F) \/ (Int (Cl (union F))) as Element of (Domains_Lattice T) by Th86;
A4: for b being Element of (Domains_Lattice T) st X is_less_than b holds
a [= b
proof
let b be Element of (Domains_Lattice T); ::_thesis: ( X is_less_than b implies a [= b )
reconsider B = b as Element of Domains_of T by Th86;
assume A5: X is_less_than b ; ::_thesis: a [= b
A6: for C being Subset of T st C in F holds
C c= B
proof
let C be Subset of T; ::_thesis: ( C in F implies C c= B )
reconsider C1 = C as Subset of T ;
assume A7: C in F ; ::_thesis: C c= B
then C1 is condensed by A2, Def2;
then C in { P where P is Subset of T : P is condensed } ;
then A8: C in Domains_of T by TDLAT_1:def_1;
then reconsider c = C as Element of (Domains_Lattice T) by Th86;
c [= b by A5, A7, LATTICE3:def_17;
hence C c= B by A8, Th89; ::_thesis: verum
end;
B in Domains_of T ;
then B in { C where C is Subset of T : C is condensed } by TDLAT_1:def_1;
then ex C being Subset of T st
( C = B & C is condensed ) ;
then (union F) \/ (Int (Cl (union F))) c= B by A6, Th69;
hence a [= b by A3, Th89; ::_thesis: verum
end;
take a ; ::_thesis: ( X is_less_than a & ( for b being Element of (Domains_Lattice T) st X is_less_than b holds
a [= b ) )
X is_less_than a
proof
let b be Element of (Domains_Lattice T); :: according to LATTICE3:def_17 ::_thesis: ( not b in X or b [= a )
reconsider B = b as Element of Domains_of T by Th86;
assume b in X ; ::_thesis: b [= a
then B c= (union F) \/ (Int (Cl (union F))) by Th69;
hence b [= a by A3, Th89; ::_thesis: verum
end;
hence ( X is_less_than a & ( for b being Element of (Domains_Lattice T) st X is_less_than b holds
a [= b ) ) by A4; ::_thesis: verum
end;
theorem Th91: :: TDLAT_2:91
for T being non empty TopSpace holds Domains_Lattice T is complete
proof
let T be non empty TopSpace; ::_thesis: Domains_Lattice T is complete
thus for X being set ex a being Element of (Domains_Lattice T) st
( X is_less_than a & ( for b being Element of (Domains_Lattice T) st X is_less_than b holds
a [= b ) ) :: according to LATTICE3:def_18 ::_thesis: verum
proof
let X be set ; ::_thesis: ex a being Element of (Domains_Lattice T) st
( X is_less_than a & ( for b being Element of (Domains_Lattice T) st X is_less_than b holds
a [= b ) )
set Y = { c where c is Element of (Domains_Lattice T) : c in X } ;
A1: for d being Element of (Domains_Lattice T) st { c where c is Element of (Domains_Lattice T) : c in X } is_less_than d holds
X is_less_than d
proof
let d be Element of (Domains_Lattice T); ::_thesis: ( { c where c is Element of (Domains_Lattice T) : c in X } is_less_than d implies X is_less_than d )
assume A2: { c where c is Element of (Domains_Lattice T) : c in X } is_less_than d ; ::_thesis: X is_less_than d
thus for e being Element of (Domains_Lattice T) st e in X holds
e [= d :: according to LATTICE3:def_17 ::_thesis: verum
proof
let e be Element of (Domains_Lattice T); ::_thesis: ( e in X implies e [= d )
assume e in X ; ::_thesis: e [= d
then e in { c where c is Element of (Domains_Lattice T) : c in X } ;
hence e [= d by A2, LATTICE3:def_17; ::_thesis: verum
end;
end;
A3: for d being Element of (Domains_Lattice T) st X is_less_than d holds
{ c where c is Element of (Domains_Lattice T) : c in X } is_less_than d
proof
let d be Element of (Domains_Lattice T); ::_thesis: ( X is_less_than d implies { c where c is Element of (Domains_Lattice T) : c in X } is_less_than d )
assume A4: X is_less_than d ; ::_thesis: { c where c is Element of (Domains_Lattice T) : c in X } is_less_than d
thus for e being Element of (Domains_Lattice T) st e in { c where c is Element of (Domains_Lattice T) : c in X } holds
e [= d :: according to LATTICE3:def_17 ::_thesis: verum
proof
let e be Element of (Domains_Lattice T); ::_thesis: ( e in { c where c is Element of (Domains_Lattice T) : c in X } implies e [= d )
assume e in { c where c is Element of (Domains_Lattice T) : c in X } ; ::_thesis: e [= d
then ex e0 being Element of (Domains_Lattice T) st
( e0 = e & e0 in X ) ;
hence e [= d by A4, LATTICE3:def_17; ::_thesis: verum
end;
end;
now__::_thesis:_for_x_being_set_st_x_in__{__c_where_c_is_Element_of_(Domains_Lattice_T)_:_c_in_X__}__holds_
x_in_the_carrier_of_(Domains_Lattice_T)
let x be set ; ::_thesis: ( x in { c where c is Element of (Domains_Lattice T) : c in X } implies x in the carrier of (Domains_Lattice T) )
assume x in { c where c is Element of (Domains_Lattice T) : c in X } ; ::_thesis: x in the carrier of (Domains_Lattice T)
then ex y being Element of (Domains_Lattice T) st
( y = x & y in X ) ;
hence x in the carrier of (Domains_Lattice T) ; ::_thesis: verum
end;
then reconsider Y = { c where c is Element of (Domains_Lattice T) : c in X } as Subset of (Domains_Lattice T) by TARSKI:def_3;
consider a being Element of (Domains_Lattice T) such that
A5: Y is_less_than a and
A6: for b being Element of (Domains_Lattice T) st Y is_less_than b holds
a [= b by Th90;
take a ; ::_thesis: ( X is_less_than a & ( for b being Element of (Domains_Lattice T) st X is_less_than b holds
a [= b ) )
for b being Element of (Domains_Lattice T) st X is_less_than b holds
a [= b by A3, A6;
hence ( X is_less_than a & ( for b being Element of (Domains_Lattice T) st X is_less_than b holds
a [= b ) ) by A1, A5; ::_thesis: verum
end;
end;
theorem Th92: :: TDLAT_2:92
for T being non empty TopSpace
for F being Subset-Family of T st F is domains-family holds
for X being Subset of (Domains_Lattice T) st X = F holds
"\/" (X,(Domains_Lattice T)) = (union F) \/ (Int (Cl (union F)))
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st F is domains-family holds
for X being Subset of (Domains_Lattice T) st X = F holds
"\/" (X,(Domains_Lattice T)) = (union F) \/ (Int (Cl (union F)))
let F be Subset-Family of T; ::_thesis: ( F is domains-family implies for X being Subset of (Domains_Lattice T) st X = F holds
"\/" (X,(Domains_Lattice T)) = (union F) \/ (Int (Cl (union F))) )
assume A1: F is domains-family ; ::_thesis: for X being Subset of (Domains_Lattice T) st X = F holds
"\/" (X,(Domains_Lattice T)) = (union F) \/ (Int (Cl (union F)))
let X be Subset of (Domains_Lattice T); ::_thesis: ( X = F implies "\/" (X,(Domains_Lattice T)) = (union F) \/ (Int (Cl (union F))) )
assume A2: X = F ; ::_thesis: "\/" (X,(Domains_Lattice T)) = (union F) \/ (Int (Cl (union F)))
thus "\/" (X,(Domains_Lattice T)) = (union F) \/ (Int (Cl (union F))) ::_thesis: verum
proof
set A = (union F) \/ (Int (Cl (union F)));
(union F) \/ (Int (Cl (union F))) is condensed by A1, Th68;
then (union F) \/ (Int (Cl (union F))) in { C where C is Subset of T : C is condensed } ;
then A3: (union F) \/ (Int (Cl (union F))) in Domains_of T by TDLAT_1:def_1;
then reconsider a = (union F) \/ (Int (Cl (union F))) as Element of (Domains_Lattice T) by Th86;
A4: X is_less_than a
proof
let b be Element of (Domains_Lattice T); :: according to LATTICE3:def_17 ::_thesis: ( not b in X or b [= a )
reconsider B = b as Element of Domains_of T by Th86;
assume b in X ; ::_thesis: b [= a
then B c= (union F) \/ (Int (Cl (union F))) by A2, Th69;
hence b [= a by A3, Th89; ::_thesis: verum
end;
A5: for b being Element of (Domains_Lattice T) st X is_less_than b holds
a [= b
proof
let b be Element of (Domains_Lattice T); ::_thesis: ( X is_less_than b implies a [= b )
reconsider B = b as Element of Domains_of T by Th86;
assume A6: X is_less_than b ; ::_thesis: a [= b
A7: for C being Subset of T st C in F holds
C c= B
proof
let C be Subset of T; ::_thesis: ( C in F implies C c= B )
reconsider C1 = C as Subset of T ;
assume A8: C in F ; ::_thesis: C c= B
then C1 is condensed by A1, Def2;
then C in { P where P is Subset of T : P is condensed } ;
then A9: C in Domains_of T by TDLAT_1:def_1;
then reconsider c = C as Element of (Domains_Lattice T) by Th86;
c [= b by A2, A6, A8, LATTICE3:def_17;
hence C c= B by A9, Th89; ::_thesis: verum
end;
B in Domains_of T ;
then B in { C where C is Subset of T : C is condensed } by TDLAT_1:def_1;
then ex C being Subset of T st
( C = B & C is condensed ) ;
then (union F) \/ (Int (Cl (union F))) c= B by A7, Th69;
hence a [= b by A3, Th89; ::_thesis: verum
end;
Domains_Lattice T is complete by Th91;
hence "\/" (X,(Domains_Lattice T)) = (union F) \/ (Int (Cl (union F))) by A4, A5, LATTICE3:def_21; ::_thesis: verum
end;
end;
theorem Th93: :: TDLAT_2:93
for T being non empty TopSpace
for F being Subset-Family of T st F is domains-family holds
for X being Subset of (Domains_Lattice T) st X = F holds
( ( X <> {} implies "/\" (X,(Domains_Lattice T)) = (meet F) /\ (Cl (Int (meet F))) ) & ( X = {} implies "/\" (X,(Domains_Lattice T)) = [#] T ) )
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st F is domains-family holds
for X being Subset of (Domains_Lattice T) st X = F holds
( ( X <> {} implies "/\" (X,(Domains_Lattice T)) = (meet F) /\ (Cl (Int (meet F))) ) & ( X = {} implies "/\" (X,(Domains_Lattice T)) = [#] T ) )
let F be Subset-Family of T; ::_thesis: ( F is domains-family implies for X being Subset of (Domains_Lattice T) st X = F holds
( ( X <> {} implies "/\" (X,(Domains_Lattice T)) = (meet F) /\ (Cl (Int (meet F))) ) & ( X = {} implies "/\" (X,(Domains_Lattice T)) = [#] T ) ) )
assume A1: F is domains-family ; ::_thesis: for X being Subset of (Domains_Lattice T) st X = F holds
( ( X <> {} implies "/\" (X,(Domains_Lattice T)) = (meet F) /\ (Cl (Int (meet F))) ) & ( X = {} implies "/\" (X,(Domains_Lattice T)) = [#] T ) )
let X be Subset of (Domains_Lattice T); ::_thesis: ( X = F implies ( ( X <> {} implies "/\" (X,(Domains_Lattice T)) = (meet F) /\ (Cl (Int (meet F))) ) & ( X = {} implies "/\" (X,(Domains_Lattice T)) = [#] T ) ) )
assume A2: X = F ; ::_thesis: ( ( X <> {} implies "/\" (X,(Domains_Lattice T)) = (meet F) /\ (Cl (Int (meet F))) ) & ( X = {} implies "/\" (X,(Domains_Lattice T)) = [#] T ) )
thus ( X <> {} implies "/\" (X,(Domains_Lattice T)) = (meet F) /\ (Cl (Int (meet F))) ) ::_thesis: ( X = {} implies "/\" (X,(Domains_Lattice T)) = [#] T )
proof
set A = (meet F) /\ (Cl (Int (meet F)));
(meet F) /\ (Cl (Int (meet F))) is condensed by A1, Th70;
then (meet F) /\ (Cl (Int (meet F))) in { C where C is Subset of T : C is condensed } ;
then A3: (meet F) /\ (Cl (Int (meet F))) in Domains_of T by TDLAT_1:def_1;
then reconsider a = (meet F) /\ (Cl (Int (meet F))) as Element of (Domains_Lattice T) by Th86;
A4: a is_less_than X
proof
let b be Element of (Domains_Lattice T); :: according to LATTICE3:def_16 ::_thesis: ( not b in X or a [= b )
reconsider B = b as Element of Domains_of T by Th86;
assume b in X ; ::_thesis: a [= b
then (meet F) /\ (Cl (Int (meet F))) c= B by A2, Th71;
hence a [= b by A3, Th89; ::_thesis: verum
end;
assume A5: X <> {} ; ::_thesis: "/\" (X,(Domains_Lattice T)) = (meet F) /\ (Cl (Int (meet F)))
A6: for b being Element of (Domains_Lattice T) st b is_less_than X holds
b [= a
proof
let b be Element of (Domains_Lattice T); ::_thesis: ( b is_less_than X implies b [= a )
reconsider B = b as Element of Domains_of T by Th86;
assume A7: b is_less_than X ; ::_thesis: b [= a
A8: for C being Subset of T st C in F holds
B c= C
proof
let C be Subset of T; ::_thesis: ( C in F implies B c= C )
reconsider C1 = C as Subset of T ;
assume A9: C in F ; ::_thesis: B c= C
then C1 is condensed by A1, Def2;
then C in { P where P is Subset of T : P is condensed } ;
then A10: C in Domains_of T by TDLAT_1:def_1;
then reconsider c = C as Element of (Domains_Lattice T) by Th86;
b [= c by A2, A7, A9, LATTICE3:def_16;
hence B c= C by A10, Th89; ::_thesis: verum
end;
B in Domains_of T ;
then B in { C where C is Subset of T : C is condensed } by TDLAT_1:def_1;
then ex C being Subset of T st
( C = B & C is condensed ) ;
then B c= (meet F) /\ (Cl (Int (meet F))) by A2, A5, A8, Th71;
hence b [= a by A3, Th89; ::_thesis: verum
end;
Domains_Lattice T is complete by Th91;
hence "/\" (X,(Domains_Lattice T)) = (meet F) /\ (Cl (Int (meet F))) by A4, A6, LATTICE3:34; ::_thesis: verum
end;
thus ( X = {} implies "/\" (X,(Domains_Lattice T)) = [#] T ) ::_thesis: verum
proof
set A = [#] T;
[#] T is condensed by TDLAT_1:15;
then [#] T in { C where C is Subset of T : C is condensed } ;
then A11: [#] T in Domains_of T by TDLAT_1:def_1;
then reconsider a = [#] T as Element of (Domains_Lattice T) by Th86;
A12: for b being Element of (Domains_Lattice T) st b is_less_than X holds
b [= a
proof
let b be Element of (Domains_Lattice T); ::_thesis: ( b is_less_than X implies b [= a )
reconsider B = b as Element of Domains_of T by Th86;
assume b is_less_than X ; ::_thesis: b [= a
B c= [#] T ;
hence b [= a by A11, Th89; ::_thesis: verum
end;
assume A13: X = {} ; ::_thesis: "/\" (X,(Domains_Lattice T)) = [#] T
A14: a is_less_than X
proof
let b be Element of (Domains_Lattice T); :: according to LATTICE3:def_16 ::_thesis: ( not b in X or a [= b )
assume b in X ; ::_thesis: a [= b
hence a [= b by A13; ::_thesis: verum
end;
Domains_Lattice T is complete by Th91;
hence "/\" (X,(Domains_Lattice T)) = [#] T by A14, A12, LATTICE3:34; ::_thesis: verum
end;
end;
begin
theorem Th94: :: TDLAT_2:94
for T being non empty TopSpace holds the carrier of (Closed_Domains_Lattice T) = Closed_Domains_of T
proof
let T be non empty TopSpace; ::_thesis: the carrier of (Closed_Domains_Lattice T) = Closed_Domains_of T
Closed_Domains_Lattice T = LattStr(# (Closed_Domains_of T),(CLD-Union T),(CLD-Meet T) #) by TDLAT_1:def_8;
hence the carrier of (Closed_Domains_Lattice T) = Closed_Domains_of T ; ::_thesis: verum
end;
theorem Th95: :: TDLAT_2:95
for T being non empty TopSpace
for a, b being Element of (Closed_Domains_Lattice T)
for A, B being Element of Closed_Domains_of T st a = A & b = B holds
( a "\/" b = A \/ B & a "/\" b = Cl (Int (A /\ B)) )
proof
let T be non empty TopSpace; ::_thesis: for a, b being Element of (Closed_Domains_Lattice T)
for A, B being Element of Closed_Domains_of T st a = A & b = B holds
( a "\/" b = A \/ B & a "/\" b = Cl (Int (A /\ B)) )
let a, b be Element of (Closed_Domains_Lattice T); ::_thesis: for A, B being Element of Closed_Domains_of T st a = A & b = B holds
( a "\/" b = A \/ B & a "/\" b = Cl (Int (A /\ B)) )
let A, B be Element of Closed_Domains_of T; ::_thesis: ( a = A & b = B implies ( a "\/" b = A \/ B & a "/\" b = Cl (Int (A /\ B)) ) )
assume that
A1: a = A and
A2: b = B ; ::_thesis: ( a "\/" b = A \/ B & a "/\" b = Cl (Int (A /\ B)) )
A3: Closed_Domains_Lattice T = LattStr(# (Closed_Domains_of T),(CLD-Union T),(CLD-Meet T) #) by TDLAT_1:def_8;
hence a "\/" b = (CLD-Union T) . (A,B) by A1, A2, LATTICES:def_1
.= A \/ B by TDLAT_1:def_6 ;
::_thesis: a "/\" b = Cl (Int (A /\ B))
thus a "/\" b = (CLD-Meet T) . (A,B) by A3, A1, A2, LATTICES:def_2
.= Cl (Int (A /\ B)) by TDLAT_1:def_7 ; ::_thesis: verum
end;
theorem :: TDLAT_2:96
for T being non empty TopSpace holds
( Bottom (Closed_Domains_Lattice T) = {} T & Top (Closed_Domains_Lattice T) = [#] T )
proof
let T be non empty TopSpace; ::_thesis: ( Bottom (Closed_Domains_Lattice T) = {} T & Top (Closed_Domains_Lattice T) = [#] T )
thus Bottom (Closed_Domains_Lattice T) = {} T ::_thesis: Top (Closed_Domains_Lattice T) = [#] T
proof
{} T is closed_condensed by TDLAT_1:18;
then A1: {} T in { A where A is Subset of T : A is closed_condensed } ;
then reconsider E = {} T as Element of Closed_Domains_of T by TDLAT_1:def_5;
{} T in Closed_Domains_of T by A1, TDLAT_1:def_5;
then reconsider e = {} T as Element of (Closed_Domains_Lattice T) by Th94;
for a being Element of (Closed_Domains_Lattice T) holds e "\/" a = a
proof
let a be Element of (Closed_Domains_Lattice T); ::_thesis: e "\/" a = a
reconsider A = a as Element of Closed_Domains_of T by Th94;
thus e "\/" a = E \/ A by Th95
.= a ; ::_thesis: verum
end;
hence Bottom (Closed_Domains_Lattice T) = {} T by LATTICE2:14; ::_thesis: verum
end;
thus Top (Closed_Domains_Lattice T) = [#] T ::_thesis: verum
proof
[#] T is closed_condensed by TDLAT_1:19;
then A2: [#] T in { A where A is Subset of T : A is closed_condensed } ;
then reconsider E = [#] T as Element of Closed_Domains_of T by TDLAT_1:def_5;
[#] T in Closed_Domains_of T by A2, TDLAT_1:def_5;
then reconsider e = [#] T as Element of (Closed_Domains_Lattice T) by Th94;
for a being Element of (Closed_Domains_Lattice T) holds e "/\" a = a
proof
let a be Element of (Closed_Domains_Lattice T); ::_thesis: e "/\" a = a
reconsider A = a as Element of Closed_Domains_of T by Th94;
A in Closed_Domains_of T ;
then A in { C where C is Subset of T : C is closed_condensed } by TDLAT_1:def_5;
then A3: ex D being Subset of T st
( D = A & D is closed_condensed ) ;
thus e "/\" a = Cl (Int (E /\ A)) by Th95
.= Cl (Int A) by XBOOLE_1:28
.= a by A3, TOPS_1:def_7 ; ::_thesis: verum
end;
hence Top (Closed_Domains_Lattice T) = [#] T by LATTICE2:16; ::_thesis: verum
end;
end;
theorem Th97: :: TDLAT_2:97
for T being non empty TopSpace
for a, b being Element of (Closed_Domains_Lattice T)
for A, B being Element of Closed_Domains_of T st a = A & b = B holds
( a [= b iff A c= B )
proof
let T be non empty TopSpace; ::_thesis: for a, b being Element of (Closed_Domains_Lattice T)
for A, B being Element of Closed_Domains_of T st a = A & b = B holds
( a [= b iff A c= B )
let a, b be Element of (Closed_Domains_Lattice T); ::_thesis: for A, B being Element of Closed_Domains_of T st a = A & b = B holds
( a [= b iff A c= B )
let A, B be Element of Closed_Domains_of T; ::_thesis: ( a = A & b = B implies ( a [= b iff A c= B ) )
assume that
A1: a = A and
A2: b = B ; ::_thesis: ( a [= b iff A c= B )
thus ( a [= b implies A c= B ) ::_thesis: ( A c= B implies a [= b )
proof
assume a [= b ; ::_thesis: A c= B
then a "\/" b = b by LATTICES:def_3;
then A \/ B = B by A1, A2, Th95;
hence A c= B by XBOOLE_1:7; ::_thesis: verum
end;
thus ( A c= B implies a [= b ) ::_thesis: verum
proof
assume A c= B ; ::_thesis: a [= b
then A \/ B = B by XBOOLE_1:12;
then a "\/" b = b by A1, A2, Th95;
hence a [= b by LATTICES:def_3; ::_thesis: verum
end;
end;
theorem Th98: :: TDLAT_2:98
for T being non empty TopSpace
for X being Subset of (Closed_Domains_Lattice T) ex a being Element of (Closed_Domains_Lattice T) st
( X is_less_than a & ( for b being Element of (Closed_Domains_Lattice T) st X is_less_than b holds
a [= b ) )
proof
let T be non empty TopSpace; ::_thesis: for X being Subset of (Closed_Domains_Lattice T) ex a being Element of (Closed_Domains_Lattice T) st
( X is_less_than a & ( for b being Element of (Closed_Domains_Lattice T) st X is_less_than b holds
a [= b ) )
let X be Subset of (Closed_Domains_Lattice T); ::_thesis: ex a being Element of (Closed_Domains_Lattice T) st
( X is_less_than a & ( for b being Element of (Closed_Domains_Lattice T) st X is_less_than b holds
a [= b ) )
X c= the carrier of (Closed_Domains_Lattice T) ;
then A1: X c= Closed_Domains_of T by Th94;
then reconsider F = X as Subset-Family of T by TOPS_2:2;
set A = Cl (union F);
A2: F is closed-domains-family by A1, Th72;
then Cl (union F) is closed_condensed by Th76;
then Cl (union F) in { C where C is Subset of T : C is closed_condensed } ;
then A3: Cl (union F) in Closed_Domains_of T by TDLAT_1:def_5;
then reconsider a = Cl (union F) as Element of (Closed_Domains_Lattice T) by Th94;
A4: for b being Element of (Closed_Domains_Lattice T) st X is_less_than b holds
a [= b
proof
let b be Element of (Closed_Domains_Lattice T); ::_thesis: ( X is_less_than b implies a [= b )
reconsider B = b as Element of Closed_Domains_of T by Th94;
assume A5: X is_less_than b ; ::_thesis: a [= b
A6: for C being Subset of T st C in F holds
C c= B
proof
let C be Subset of T; ::_thesis: ( C in F implies C c= B )
reconsider C1 = C as Subset of T ;
assume A7: C in F ; ::_thesis: C c= B
then C1 is closed_condensed by A2, Def3;
then C in { P where P is Subset of T : P is closed_condensed } ;
then A8: C in Closed_Domains_of T by TDLAT_1:def_5;
then reconsider c = C as Element of (Closed_Domains_Lattice T) by Th94;
c [= b by A5, A7, LATTICE3:def_17;
hence C c= B by A8, Th97; ::_thesis: verum
end;
B in Closed_Domains_of T ;
then B in { C where C is Subset of T : C is closed_condensed } by TDLAT_1:def_5;
then ex C being Subset of T st
( C = B & C is closed_condensed ) ;
then Cl (union F) c= B by A6, Th77;
hence a [= b by A3, Th97; ::_thesis: verum
end;
take a ; ::_thesis: ( X is_less_than a & ( for b being Element of (Closed_Domains_Lattice T) st X is_less_than b holds
a [= b ) )
X is_less_than a
proof
let b be Element of (Closed_Domains_Lattice T); :: according to LATTICE3:def_17 ::_thesis: ( not b in X or b [= a )
reconsider B = b as Element of Closed_Domains_of T by Th94;
assume b in X ; ::_thesis: b [= a
then B c= Cl (union F) by Th77;
hence b [= a by A3, Th97; ::_thesis: verum
end;
hence ( X is_less_than a & ( for b being Element of (Closed_Domains_Lattice T) st X is_less_than b holds
a [= b ) ) by A4; ::_thesis: verum
end;
theorem Th99: :: TDLAT_2:99
for T being non empty TopSpace holds Closed_Domains_Lattice T is complete
proof
let T be non empty TopSpace; ::_thesis: Closed_Domains_Lattice T is complete
thus for X being set ex a being Element of (Closed_Domains_Lattice T) st
( X is_less_than a & ( for b being Element of (Closed_Domains_Lattice T) st X is_less_than b holds
a [= b ) ) :: according to LATTICE3:def_18 ::_thesis: verum
proof
let X be set ; ::_thesis: ex a being Element of (Closed_Domains_Lattice T) st
( X is_less_than a & ( for b being Element of (Closed_Domains_Lattice T) st X is_less_than b holds
a [= b ) )
set Y = { c where c is Element of (Closed_Domains_Lattice T) : c in X } ;
A1: for d being Element of (Closed_Domains_Lattice T) st { c where c is Element of (Closed_Domains_Lattice T) : c in X } is_less_than d holds
X is_less_than d
proof
let d be Element of (Closed_Domains_Lattice T); ::_thesis: ( { c where c is Element of (Closed_Domains_Lattice T) : c in X } is_less_than d implies X is_less_than d )
assume A2: { c where c is Element of (Closed_Domains_Lattice T) : c in X } is_less_than d ; ::_thesis: X is_less_than d
thus for e being Element of (Closed_Domains_Lattice T) st e in X holds
e [= d :: according to LATTICE3:def_17 ::_thesis: verum
proof
let e be Element of (Closed_Domains_Lattice T); ::_thesis: ( e in X implies e [= d )
assume e in X ; ::_thesis: e [= d
then e in { c where c is Element of (Closed_Domains_Lattice T) : c in X } ;
hence e [= d by A2, LATTICE3:def_17; ::_thesis: verum
end;
end;
A3: for d being Element of (Closed_Domains_Lattice T) st X is_less_than d holds
{ c where c is Element of (Closed_Domains_Lattice T) : c in X } is_less_than d
proof
let d be Element of (Closed_Domains_Lattice T); ::_thesis: ( X is_less_than d implies { c where c is Element of (Closed_Domains_Lattice T) : c in X } is_less_than d )
assume A4: X is_less_than d ; ::_thesis: { c where c is Element of (Closed_Domains_Lattice T) : c in X } is_less_than d
thus for e being Element of (Closed_Domains_Lattice T) st e in { c where c is Element of (Closed_Domains_Lattice T) : c in X } holds
e [= d :: according to LATTICE3:def_17 ::_thesis: verum
proof
let e be Element of (Closed_Domains_Lattice T); ::_thesis: ( e in { c where c is Element of (Closed_Domains_Lattice T) : c in X } implies e [= d )
assume e in { c where c is Element of (Closed_Domains_Lattice T) : c in X } ; ::_thesis: e [= d
then ex e0 being Element of (Closed_Domains_Lattice T) st
( e0 = e & e0 in X ) ;
hence e [= d by A4, LATTICE3:def_17; ::_thesis: verum
end;
end;
now__::_thesis:_for_x_being_set_st_x_in__{__c_where_c_is_Element_of_(Closed_Domains_Lattice_T)_:_c_in_X__}__holds_
x_in_the_carrier_of_(Closed_Domains_Lattice_T)
let x be set ; ::_thesis: ( x in { c where c is Element of (Closed_Domains_Lattice T) : c in X } implies x in the carrier of (Closed_Domains_Lattice T) )
assume x in { c where c is Element of (Closed_Domains_Lattice T) : c in X } ; ::_thesis: x in the carrier of (Closed_Domains_Lattice T)
then ex y being Element of (Closed_Domains_Lattice T) st
( y = x & y in X ) ;
hence x in the carrier of (Closed_Domains_Lattice T) ; ::_thesis: verum
end;
then reconsider Y = { c where c is Element of (Closed_Domains_Lattice T) : c in X } as Subset of (Closed_Domains_Lattice T) by TARSKI:def_3;
consider a being Element of (Closed_Domains_Lattice T) such that
A5: Y is_less_than a and
A6: for b being Element of (Closed_Domains_Lattice T) st Y is_less_than b holds
a [= b by Th98;
take a ; ::_thesis: ( X is_less_than a & ( for b being Element of (Closed_Domains_Lattice T) st X is_less_than b holds
a [= b ) )
for b being Element of (Closed_Domains_Lattice T) st X is_less_than b holds
a [= b by A3, A6;
hence ( X is_less_than a & ( for b being Element of (Closed_Domains_Lattice T) st X is_less_than b holds
a [= b ) ) by A1, A5; ::_thesis: verum
end;
end;
theorem :: TDLAT_2:100
for T being non empty TopSpace
for F being Subset-Family of T st F is closed-domains-family holds
for X being Subset of (Closed_Domains_Lattice T) st X = F holds
"\/" (X,(Closed_Domains_Lattice T)) = Cl (union F)
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st F is closed-domains-family holds
for X being Subset of (Closed_Domains_Lattice T) st X = F holds
"\/" (X,(Closed_Domains_Lattice T)) = Cl (union F)
let F be Subset-Family of T; ::_thesis: ( F is closed-domains-family implies for X being Subset of (Closed_Domains_Lattice T) st X = F holds
"\/" (X,(Closed_Domains_Lattice T)) = Cl (union F) )
assume A1: F is closed-domains-family ; ::_thesis: for X being Subset of (Closed_Domains_Lattice T) st X = F holds
"\/" (X,(Closed_Domains_Lattice T)) = Cl (union F)
let X be Subset of (Closed_Domains_Lattice T); ::_thesis: ( X = F implies "\/" (X,(Closed_Domains_Lattice T)) = Cl (union F) )
assume A2: X = F ; ::_thesis: "\/" (X,(Closed_Domains_Lattice T)) = Cl (union F)
thus "\/" (X,(Closed_Domains_Lattice T)) = Cl (union F) ::_thesis: verum
proof
set A = Cl (union F);
Cl (union F) is closed_condensed by A1, Th76;
then Cl (union F) in { C where C is Subset of T : C is closed_condensed } ;
then A3: Cl (union F) in Closed_Domains_of T by TDLAT_1:def_5;
then reconsider a = Cl (union F) as Element of (Closed_Domains_Lattice T) by Th94;
A4: X is_less_than a
proof
let b be Element of (Closed_Domains_Lattice T); :: according to LATTICE3:def_17 ::_thesis: ( not b in X or b [= a )
reconsider B = b as Element of Closed_Domains_of T by Th94;
assume b in X ; ::_thesis: b [= a
then B c= Cl (union F) by A2, Th77;
hence b [= a by A3, Th97; ::_thesis: verum
end;
A5: for b being Element of (Closed_Domains_Lattice T) st X is_less_than b holds
a [= b
proof
let b be Element of (Closed_Domains_Lattice T); ::_thesis: ( X is_less_than b implies a [= b )
reconsider B = b as Element of Closed_Domains_of T by Th94;
assume A6: X is_less_than b ; ::_thesis: a [= b
A7: for C being Subset of T st C in F holds
C c= B
proof
let C be Subset of T; ::_thesis: ( C in F implies C c= B )
reconsider C1 = C as Subset of T ;
assume A8: C in F ; ::_thesis: C c= B
then C1 is closed_condensed by A1, Def3;
then C in { P where P is Subset of T : P is closed_condensed } ;
then A9: C in Closed_Domains_of T by TDLAT_1:def_5;
then reconsider c = C as Element of (Closed_Domains_Lattice T) by Th94;
c [= b by A2, A6, A8, LATTICE3:def_17;
hence C c= B by A9, Th97; ::_thesis: verum
end;
B in Closed_Domains_of T ;
then B in { C where C is Subset of T : C is closed_condensed } by TDLAT_1:def_5;
then ex C being Subset of T st
( C = B & C is closed_condensed ) ;
then Cl (union F) c= B by A7, Th77;
hence a [= b by A3, Th97; ::_thesis: verum
end;
Closed_Domains_Lattice T is complete by Th99;
hence "\/" (X,(Closed_Domains_Lattice T)) = Cl (union F) by A4, A5, LATTICE3:def_21; ::_thesis: verum
end;
end;
theorem :: TDLAT_2:101
for T being non empty TopSpace
for F being Subset-Family of T st F is closed-domains-family holds
for X being Subset of (Closed_Domains_Lattice T) st X = F holds
( ( X <> {} implies "/\" (X,(Closed_Domains_Lattice T)) = Cl (Int (meet F)) ) & ( X = {} implies "/\" (X,(Closed_Domains_Lattice T)) = [#] T ) )
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st F is closed-domains-family holds
for X being Subset of (Closed_Domains_Lattice T) st X = F holds
( ( X <> {} implies "/\" (X,(Closed_Domains_Lattice T)) = Cl (Int (meet F)) ) & ( X = {} implies "/\" (X,(Closed_Domains_Lattice T)) = [#] T ) )
let F be Subset-Family of T; ::_thesis: ( F is closed-domains-family implies for X being Subset of (Closed_Domains_Lattice T) st X = F holds
( ( X <> {} implies "/\" (X,(Closed_Domains_Lattice T)) = Cl (Int (meet F)) ) & ( X = {} implies "/\" (X,(Closed_Domains_Lattice T)) = [#] T ) ) )
assume A1: F is closed-domains-family ; ::_thesis: for X being Subset of (Closed_Domains_Lattice T) st X = F holds
( ( X <> {} implies "/\" (X,(Closed_Domains_Lattice T)) = Cl (Int (meet F)) ) & ( X = {} implies "/\" (X,(Closed_Domains_Lattice T)) = [#] T ) )
let X be Subset of (Closed_Domains_Lattice T); ::_thesis: ( X = F implies ( ( X <> {} implies "/\" (X,(Closed_Domains_Lattice T)) = Cl (Int (meet F)) ) & ( X = {} implies "/\" (X,(Closed_Domains_Lattice T)) = [#] T ) ) )
assume A2: X = F ; ::_thesis: ( ( X <> {} implies "/\" (X,(Closed_Domains_Lattice T)) = Cl (Int (meet F)) ) & ( X = {} implies "/\" (X,(Closed_Domains_Lattice T)) = [#] T ) )
thus ( X <> {} implies "/\" (X,(Closed_Domains_Lattice T)) = Cl (Int (meet F)) ) ::_thesis: ( X = {} implies "/\" (X,(Closed_Domains_Lattice T)) = [#] T )
proof
set A = Cl (Int (meet F));
Cl (Int (meet F)) is closed_condensed by A1, Th76;
then Cl (Int (meet F)) in { C where C is Subset of T : C is closed_condensed } ;
then A3: Cl (Int (meet F)) in Closed_Domains_of T by TDLAT_1:def_5;
then reconsider a = Cl (Int (meet F)) as Element of (Closed_Domains_Lattice T) by Th94;
A4: a is_less_than X
proof
let b be Element of (Closed_Domains_Lattice T); :: according to LATTICE3:def_16 ::_thesis: ( not b in X or a [= b )
reconsider B = b as Element of Closed_Domains_of T by Th94;
assume b in X ; ::_thesis: a [= b
then Cl (Int (meet F)) c= B by A1, A2, Th74, Th78;
hence a [= b by A3, Th97; ::_thesis: verum
end;
assume A5: X <> {} ; ::_thesis: "/\" (X,(Closed_Domains_Lattice T)) = Cl (Int (meet F))
A6: for b being Element of (Closed_Domains_Lattice T) st b is_less_than X holds
b [= a
proof
let b be Element of (Closed_Domains_Lattice T); ::_thesis: ( b is_less_than X implies b [= a )
reconsider B = b as Element of Closed_Domains_of T by Th94;
assume A7: b is_less_than X ; ::_thesis: b [= a
A8: for C being Subset of T st C in F holds
B c= C
proof
let C be Subset of T; ::_thesis: ( C in F implies B c= C )
reconsider C1 = C as Subset of T ;
assume A9: C in F ; ::_thesis: B c= C
then C1 is closed_condensed by A1, Def3;
then C in { P where P is Subset of T : P is closed_condensed } ;
then A10: C in Closed_Domains_of T by TDLAT_1:def_5;
then reconsider c = C as Element of (Closed_Domains_Lattice T) by Th94;
b [= c by A2, A7, A9, LATTICE3:def_16;
hence B c= C by A10, Th97; ::_thesis: verum
end;
B in Closed_Domains_of T ;
then B in { C where C is Subset of T : C is closed_condensed } by TDLAT_1:def_5;
then ex C being Subset of T st
( C = B & C is closed_condensed ) ;
then B c= Cl (Int (meet F)) by A2, A5, A8, Th78;
hence b [= a by A3, Th97; ::_thesis: verum
end;
Closed_Domains_Lattice T is complete by Th99;
hence "/\" (X,(Closed_Domains_Lattice T)) = Cl (Int (meet F)) by A4, A6, LATTICE3:34; ::_thesis: verum
end;
thus ( X = {} implies "/\" (X,(Closed_Domains_Lattice T)) = [#] T ) ::_thesis: verum
proof
set A = [#] T;
[#] T is closed_condensed by TDLAT_1:19;
then [#] T in { C where C is Subset of T : C is closed_condensed } ;
then A11: [#] T in Closed_Domains_of T by TDLAT_1:def_5;
then reconsider a = [#] T as Element of (Closed_Domains_Lattice T) by Th94;
A12: for b being Element of (Closed_Domains_Lattice T) st b is_less_than X holds
b [= a
proof
let b be Element of (Closed_Domains_Lattice T); ::_thesis: ( b is_less_than X implies b [= a )
reconsider B = b as Element of Closed_Domains_of T by Th94;
assume b is_less_than X ; ::_thesis: b [= a
B c= [#] T ;
hence b [= a by A11, Th97; ::_thesis: verum
end;
assume A13: X = {} ; ::_thesis: "/\" (X,(Closed_Domains_Lattice T)) = [#] T
A14: a is_less_than X
proof
let b be Element of (Closed_Domains_Lattice T); :: according to LATTICE3:def_16 ::_thesis: ( not b in X or a [= b )
assume b in X ; ::_thesis: a [= b
hence a [= b by A13; ::_thesis: verum
end;
Closed_Domains_Lattice T is complete by Th99;
hence "/\" (X,(Closed_Domains_Lattice T)) = [#] T by A14, A12, LATTICE3:34; ::_thesis: verum
end;
end;
theorem :: TDLAT_2:102
for T being non empty TopSpace
for F being Subset-Family of T st F is closed-domains-family holds
for X being Subset of (Domains_Lattice T) st X = F holds
( ( X <> {} implies "/\" (X,(Domains_Lattice T)) = Cl (Int (meet F)) ) & ( X = {} implies "/\" (X,(Domains_Lattice T)) = [#] T ) )
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st F is closed-domains-family holds
for X being Subset of (Domains_Lattice T) st X = F holds
( ( X <> {} implies "/\" (X,(Domains_Lattice T)) = Cl (Int (meet F)) ) & ( X = {} implies "/\" (X,(Domains_Lattice T)) = [#] T ) )
let F be Subset-Family of T; ::_thesis: ( F is closed-domains-family implies for X being Subset of (Domains_Lattice T) st X = F holds
( ( X <> {} implies "/\" (X,(Domains_Lattice T)) = Cl (Int (meet F)) ) & ( X = {} implies "/\" (X,(Domains_Lattice T)) = [#] T ) ) )
A1: Cl (Int (meet F)) c= Cl (meet F) by PRE_TOPC:19, TOPS_1:16;
assume A2: F is closed-domains-family ; ::_thesis: for X being Subset of (Domains_Lattice T) st X = F holds
( ( X <> {} implies "/\" (X,(Domains_Lattice T)) = Cl (Int (meet F)) ) & ( X = {} implies "/\" (X,(Domains_Lattice T)) = [#] T ) )
then A3: F is domains-family by Th73;
let X be Subset of (Domains_Lattice T); ::_thesis: ( X = F implies ( ( X <> {} implies "/\" (X,(Domains_Lattice T)) = Cl (Int (meet F)) ) & ( X = {} implies "/\" (X,(Domains_Lattice T)) = [#] T ) ) )
assume A4: X = F ; ::_thesis: ( ( X <> {} implies "/\" (X,(Domains_Lattice T)) = Cl (Int (meet F)) ) & ( X = {} implies "/\" (X,(Domains_Lattice T)) = [#] T ) )
meet F is closed by A2, Th74, TOPS_2:22;
then Cl (Int (meet F)) c= meet F by A1, PRE_TOPC:22;
then (meet F) /\ (Cl (Int (meet F))) = Cl (Int (meet F)) by XBOOLE_1:28;
hence ( X <> {} implies "/\" (X,(Domains_Lattice T)) = Cl (Int (meet F)) ) by A3, A4, Th93; ::_thesis: ( X = {} implies "/\" (X,(Domains_Lattice T)) = [#] T )
thus ( X = {} implies "/\" (X,(Domains_Lattice T)) = [#] T ) by A3, A4, Th93; ::_thesis: verum
end;
theorem Th103: :: TDLAT_2:103
for T being non empty TopSpace holds the carrier of (Open_Domains_Lattice T) = Open_Domains_of T
proof
let T be non empty TopSpace; ::_thesis: the carrier of (Open_Domains_Lattice T) = Open_Domains_of T
Open_Domains_Lattice T = LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #) by TDLAT_1:def_12;
hence the carrier of (Open_Domains_Lattice T) = Open_Domains_of T ; ::_thesis: verum
end;
theorem Th104: :: TDLAT_2:104
for T being non empty TopSpace
for a, b being Element of (Open_Domains_Lattice T)
for A, B being Element of Open_Domains_of T st a = A & b = B holds
( a "\/" b = Int (Cl (A \/ B)) & a "/\" b = A /\ B )
proof
let T be non empty TopSpace; ::_thesis: for a, b being Element of (Open_Domains_Lattice T)
for A, B being Element of Open_Domains_of T st a = A & b = B holds
( a "\/" b = Int (Cl (A \/ B)) & a "/\" b = A /\ B )
let a, b be Element of (Open_Domains_Lattice T); ::_thesis: for A, B being Element of Open_Domains_of T st a = A & b = B holds
( a "\/" b = Int (Cl (A \/ B)) & a "/\" b = A /\ B )
let A, B be Element of Open_Domains_of T; ::_thesis: ( a = A & b = B implies ( a "\/" b = Int (Cl (A \/ B)) & a "/\" b = A /\ B ) )
assume that
A1: a = A and
A2: b = B ; ::_thesis: ( a "\/" b = Int (Cl (A \/ B)) & a "/\" b = A /\ B )
A3: Open_Domains_Lattice T = LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #) by TDLAT_1:def_12;
hence a "\/" b = (OPD-Union T) . (A,B) by A1, A2, LATTICES:def_1
.= Int (Cl (A \/ B)) by TDLAT_1:def_10 ;
::_thesis: a "/\" b = A /\ B
thus a "/\" b = (OPD-Meet T) . (A,B) by A3, A1, A2, LATTICES:def_2
.= A /\ B by TDLAT_1:def_11 ; ::_thesis: verum
end;
theorem :: TDLAT_2:105
for T being non empty TopSpace holds
( Bottom (Open_Domains_Lattice T) = {} T & Top (Open_Domains_Lattice T) = [#] T )
proof
let T be non empty TopSpace; ::_thesis: ( Bottom (Open_Domains_Lattice T) = {} T & Top (Open_Domains_Lattice T) = [#] T )
thus Bottom (Open_Domains_Lattice T) = {} T ::_thesis: Top (Open_Domains_Lattice T) = [#] T
proof
{} T is open_condensed by TDLAT_1:20;
then A1: {} T in { A where A is Subset of T : A is open_condensed } ;
then reconsider E = {} T as Element of Open_Domains_of T by TDLAT_1:def_9;
{} T in Open_Domains_of T by A1, TDLAT_1:def_9;
then reconsider e = {} T as Element of (Open_Domains_Lattice T) by Th103;
for a being Element of (Open_Domains_Lattice T) holds e "\/" a = a
proof
let a be Element of (Open_Domains_Lattice T); ::_thesis: e "\/" a = a
reconsider A = a as Element of Open_Domains_of T by Th103;
A in Open_Domains_of T ;
then A in { C where C is Subset of T : C is open_condensed } by TDLAT_1:def_9;
then A2: ex D being Subset of T st
( D = A & D is open_condensed ) ;
thus e "\/" a = Int (Cl (E \/ A)) by Th104
.= a by A2, TOPS_1:def_8 ; ::_thesis: verum
end;
hence Bottom (Open_Domains_Lattice T) = {} T by LATTICE2:14; ::_thesis: verum
end;
thus Top (Open_Domains_Lattice T) = [#] T ::_thesis: verum
proof
[#] T is open_condensed by TDLAT_1:21;
then A3: [#] T in { A where A is Subset of T : A is open_condensed } ;
then reconsider E = [#] T as Element of Open_Domains_of T by TDLAT_1:def_9;
[#] T in Open_Domains_of T by A3, TDLAT_1:def_9;
then reconsider e = [#] T as Element of (Open_Domains_Lattice T) by Th103;
for a being Element of (Open_Domains_Lattice T) holds e "/\" a = a
proof
let a be Element of (Open_Domains_Lattice T); ::_thesis: e "/\" a = a
reconsider A = a as Element of Open_Domains_of T by Th103;
thus e "/\" a = E /\ A by Th104
.= a by XBOOLE_1:28 ; ::_thesis: verum
end;
hence Top (Open_Domains_Lattice T) = [#] T by LATTICE2:16; ::_thesis: verum
end;
end;
theorem Th106: :: TDLAT_2:106
for T being non empty TopSpace
for a, b being Element of (Open_Domains_Lattice T)
for A, B being Element of Open_Domains_of T st a = A & b = B holds
( a [= b iff A c= B )
proof
let T be non empty TopSpace; ::_thesis: for a, b being Element of (Open_Domains_Lattice T)
for A, B being Element of Open_Domains_of T st a = A & b = B holds
( a [= b iff A c= B )
let a, b be Element of (Open_Domains_Lattice T); ::_thesis: for A, B being Element of Open_Domains_of T st a = A & b = B holds
( a [= b iff A c= B )
let A, B be Element of Open_Domains_of T; ::_thesis: ( a = A & b = B implies ( a [= b iff A c= B ) )
reconsider A1 = A as Subset of T ;
assume that
A1: a = A and
A2: b = B ; ::_thesis: ( a [= b iff A c= B )
A in Open_Domains_of T ;
then A in { C where C is Subset of T : C is open_condensed } by TDLAT_1:def_9;
then ex Q being Subset of T st
( Q = A & Q is open_condensed ) ;
then A3: A1 is open by TOPS_1:67;
thus ( a [= b implies A c= B ) ::_thesis: ( A c= B implies a [= b )
proof
assume a [= b ; ::_thesis: A c= B
then a "\/" b = b by LATTICES:def_3;
then Int (Cl (A \/ B)) = B by A1, A2, Th104;
hence A c= B by A3, Th4; ::_thesis: verum
end;
B in Open_Domains_of T ;
then B in { C where C is Subset of T : C is open_condensed } by TDLAT_1:def_9;
then A4: ex P being Subset of T st
( P = B & P is open_condensed ) ;
thus ( A c= B implies a [= b ) ::_thesis: verum
proof
assume A c= B ; ::_thesis: a [= b
then Int (Cl (A \/ B)) = B by A4, Th64;
then a "\/" b = b by A1, A2, Th104;
hence a [= b by LATTICES:def_3; ::_thesis: verum
end;
end;
theorem Th107: :: TDLAT_2:107
for T being non empty TopSpace
for X being Subset of (Open_Domains_Lattice T) ex a being Element of (Open_Domains_Lattice T) st
( X is_less_than a & ( for b being Element of (Open_Domains_Lattice T) st X is_less_than b holds
a [= b ) )
proof
let T be non empty TopSpace; ::_thesis: for X being Subset of (Open_Domains_Lattice T) ex a being Element of (Open_Domains_Lattice T) st
( X is_less_than a & ( for b being Element of (Open_Domains_Lattice T) st X is_less_than b holds
a [= b ) )
let X be Subset of (Open_Domains_Lattice T); ::_thesis: ex a being Element of (Open_Domains_Lattice T) st
( X is_less_than a & ( for b being Element of (Open_Domains_Lattice T) st X is_less_than b holds
a [= b ) )
X c= the carrier of (Open_Domains_Lattice T) ;
then A1: X c= Open_Domains_of T by Th103;
then reconsider F = X as Subset-Family of T by TOPS_2:2;
set A = Int (Cl (union F));
A2: F is open-domains-family by A1, Th79;
then Int (Cl (union F)) is open_condensed by Th83;
then Int (Cl (union F)) in { C where C is Subset of T : C is open_condensed } ;
then A3: Int (Cl (union F)) in Open_Domains_of T by TDLAT_1:def_9;
then reconsider a = Int (Cl (union F)) as Element of (Open_Domains_Lattice T) by Th103;
A4: for b being Element of (Open_Domains_Lattice T) st X is_less_than b holds
a [= b
proof
let b be Element of (Open_Domains_Lattice T); ::_thesis: ( X is_less_than b implies a [= b )
reconsider B = b as Element of Open_Domains_of T by Th103;
assume A5: X is_less_than b ; ::_thesis: a [= b
A6: for C being Subset of T st C in F holds
C c= B
proof
let C be Subset of T; ::_thesis: ( C in F implies C c= B )
reconsider C1 = C as Subset of T ;
assume A7: C in F ; ::_thesis: C c= B
then C1 is open_condensed by A2, Def4;
then C in { P where P is Subset of T : P is open_condensed } ;
then A8: C in Open_Domains_of T by TDLAT_1:def_9;
then reconsider c = C as Element of (Open_Domains_Lattice T) by Th103;
c [= b by A5, A7, LATTICE3:def_17;
hence C c= B by A8, Th106; ::_thesis: verum
end;
B in Open_Domains_of T ;
then B in { C where C is Subset of T : C is open_condensed } by TDLAT_1:def_9;
then ex C being Subset of T st
( C = B & C is open_condensed ) ;
then Int (Cl (union F)) c= B by A6, Th84;
hence a [= b by A3, Th106; ::_thesis: verum
end;
take a ; ::_thesis: ( X is_less_than a & ( for b being Element of (Open_Domains_Lattice T) st X is_less_than b holds
a [= b ) )
X is_less_than a
proof
let b be Element of (Open_Domains_Lattice T); :: according to LATTICE3:def_17 ::_thesis: ( not b in X or b [= a )
reconsider B = b as Element of Open_Domains_of T by Th103;
assume b in X ; ::_thesis: b [= a
then B c= Int (Cl (union F)) by A2, Th81, Th84;
hence b [= a by A3, Th106; ::_thesis: verum
end;
hence ( X is_less_than a & ( for b being Element of (Open_Domains_Lattice T) st X is_less_than b holds
a [= b ) ) by A4; ::_thesis: verum
end;
theorem Th108: :: TDLAT_2:108
for T being non empty TopSpace holds Open_Domains_Lattice T is complete
proof
let T be non empty TopSpace; ::_thesis: Open_Domains_Lattice T is complete
thus for X being set ex a being Element of (Open_Domains_Lattice T) st
( X is_less_than a & ( for b being Element of (Open_Domains_Lattice T) st X is_less_than b holds
a [= b ) ) :: according to LATTICE3:def_18 ::_thesis: verum
proof
let X be set ; ::_thesis: ex a being Element of (Open_Domains_Lattice T) st
( X is_less_than a & ( for b being Element of (Open_Domains_Lattice T) st X is_less_than b holds
a [= b ) )
set Y = { c where c is Element of (Open_Domains_Lattice T) : c in X } ;
A1: for d being Element of (Open_Domains_Lattice T) st { c where c is Element of (Open_Domains_Lattice T) : c in X } is_less_than d holds
X is_less_than d
proof
let d be Element of (Open_Domains_Lattice T); ::_thesis: ( { c where c is Element of (Open_Domains_Lattice T) : c in X } is_less_than d implies X is_less_than d )
assume A2: { c where c is Element of (Open_Domains_Lattice T) : c in X } is_less_than d ; ::_thesis: X is_less_than d
thus for e being Element of (Open_Domains_Lattice T) st e in X holds
e [= d :: according to LATTICE3:def_17 ::_thesis: verum
proof
let e be Element of (Open_Domains_Lattice T); ::_thesis: ( e in X implies e [= d )
assume e in X ; ::_thesis: e [= d
then e in { c where c is Element of (Open_Domains_Lattice T) : c in X } ;
hence e [= d by A2, LATTICE3:def_17; ::_thesis: verum
end;
end;
A3: for d being Element of (Open_Domains_Lattice T) st X is_less_than d holds
{ c where c is Element of (Open_Domains_Lattice T) : c in X } is_less_than d
proof
let d be Element of (Open_Domains_Lattice T); ::_thesis: ( X is_less_than d implies { c where c is Element of (Open_Domains_Lattice T) : c in X } is_less_than d )
assume A4: X is_less_than d ; ::_thesis: { c where c is Element of (Open_Domains_Lattice T) : c in X } is_less_than d
thus for e being Element of (Open_Domains_Lattice T) st e in { c where c is Element of (Open_Domains_Lattice T) : c in X } holds
e [= d :: according to LATTICE3:def_17 ::_thesis: verum
proof
let e be Element of (Open_Domains_Lattice T); ::_thesis: ( e in { c where c is Element of (Open_Domains_Lattice T) : c in X } implies e [= d )
assume e in { c where c is Element of (Open_Domains_Lattice T) : c in X } ; ::_thesis: e [= d
then ex e0 being Element of (Open_Domains_Lattice T) st
( e0 = e & e0 in X ) ;
hence e [= d by A4, LATTICE3:def_17; ::_thesis: verum
end;
end;
now__::_thesis:_for_x_being_set_st_x_in__{__c_where_c_is_Element_of_(Open_Domains_Lattice_T)_:_c_in_X__}__holds_
x_in_the_carrier_of_(Open_Domains_Lattice_T)
let x be set ; ::_thesis: ( x in { c where c is Element of (Open_Domains_Lattice T) : c in X } implies x in the carrier of (Open_Domains_Lattice T) )
assume x in { c where c is Element of (Open_Domains_Lattice T) : c in X } ; ::_thesis: x in the carrier of (Open_Domains_Lattice T)
then ex y being Element of (Open_Domains_Lattice T) st
( y = x & y in X ) ;
hence x in the carrier of (Open_Domains_Lattice T) ; ::_thesis: verum
end;
then reconsider Y = { c where c is Element of (Open_Domains_Lattice T) : c in X } as Subset of (Open_Domains_Lattice T) by TARSKI:def_3;
consider a being Element of (Open_Domains_Lattice T) such that
A5: Y is_less_than a and
A6: for b being Element of (Open_Domains_Lattice T) st Y is_less_than b holds
a [= b by Th107;
take a ; ::_thesis: ( X is_less_than a & ( for b being Element of (Open_Domains_Lattice T) st X is_less_than b holds
a [= b ) )
for b being Element of (Open_Domains_Lattice T) st X is_less_than b holds
a [= b by A3, A6;
hence ( X is_less_than a & ( for b being Element of (Open_Domains_Lattice T) st X is_less_than b holds
a [= b ) ) by A1, A5; ::_thesis: verum
end;
end;
theorem :: TDLAT_2:109
for T being non empty TopSpace
for F being Subset-Family of T st F is open-domains-family holds
for X being Subset of (Open_Domains_Lattice T) st X = F holds
"\/" (X,(Open_Domains_Lattice T)) = Int (Cl (union F))
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st F is open-domains-family holds
for X being Subset of (Open_Domains_Lattice T) st X = F holds
"\/" (X,(Open_Domains_Lattice T)) = Int (Cl (union F))
let F be Subset-Family of T; ::_thesis: ( F is open-domains-family implies for X being Subset of (Open_Domains_Lattice T) st X = F holds
"\/" (X,(Open_Domains_Lattice T)) = Int (Cl (union F)) )
assume A1: F is open-domains-family ; ::_thesis: for X being Subset of (Open_Domains_Lattice T) st X = F holds
"\/" (X,(Open_Domains_Lattice T)) = Int (Cl (union F))
let X be Subset of (Open_Domains_Lattice T); ::_thesis: ( X = F implies "\/" (X,(Open_Domains_Lattice T)) = Int (Cl (union F)) )
assume A2: X = F ; ::_thesis: "\/" (X,(Open_Domains_Lattice T)) = Int (Cl (union F))
thus "\/" (X,(Open_Domains_Lattice T)) = Int (Cl (union F)) ::_thesis: verum
proof
set A = Int (Cl (union F));
Int (Cl (union F)) is open_condensed by A1, Th83;
then Int (Cl (union F)) in { C where C is Subset of T : C is open_condensed } ;
then A3: Int (Cl (union F)) in Open_Domains_of T by TDLAT_1:def_9;
then reconsider a = Int (Cl (union F)) as Element of (Open_Domains_Lattice T) by Th103;
A4: X is_less_than a
proof
let b be Element of (Open_Domains_Lattice T); :: according to LATTICE3:def_17 ::_thesis: ( not b in X or b [= a )
reconsider B = b as Element of Open_Domains_of T by Th103;
assume b in X ; ::_thesis: b [= a
then B c= Int (Cl (union F)) by A1, A2, Th81, Th84;
hence b [= a by A3, Th106; ::_thesis: verum
end;
A5: for b being Element of (Open_Domains_Lattice T) st X is_less_than b holds
a [= b
proof
let b be Element of (Open_Domains_Lattice T); ::_thesis: ( X is_less_than b implies a [= b )
reconsider B = b as Element of Open_Domains_of T by Th103;
assume A6: X is_less_than b ; ::_thesis: a [= b
A7: for C being Subset of T st C in F holds
C c= B
proof
let C be Subset of T; ::_thesis: ( C in F implies C c= B )
reconsider C1 = C as Subset of T ;
assume A8: C in F ; ::_thesis: C c= B
then C1 is open_condensed by A1, Def4;
then C in { P where P is Subset of T : P is open_condensed } ;
then A9: C in Open_Domains_of T by TDLAT_1:def_9;
then reconsider c = C as Element of (Open_Domains_Lattice T) by Th103;
c [= b by A2, A6, A8, LATTICE3:def_17;
hence C c= B by A9, Th106; ::_thesis: verum
end;
B in Open_Domains_of T ;
then B in { C where C is Subset of T : C is open_condensed } by TDLAT_1:def_9;
then ex C being Subset of T st
( C = B & C is open_condensed ) ;
then Int (Cl (union F)) c= B by A7, Th84;
hence a [= b by A3, Th106; ::_thesis: verum
end;
Open_Domains_Lattice T is complete by Th108;
hence "\/" (X,(Open_Domains_Lattice T)) = Int (Cl (union F)) by A4, A5, LATTICE3:def_21; ::_thesis: verum
end;
end;
theorem :: TDLAT_2:110
for T being non empty TopSpace
for F being Subset-Family of T st F is open-domains-family holds
for X being Subset of (Open_Domains_Lattice T) st X = F holds
( ( X <> {} implies "/\" (X,(Open_Domains_Lattice T)) = Int (meet F) ) & ( X = {} implies "/\" (X,(Open_Domains_Lattice T)) = [#] T ) )
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st F is open-domains-family holds
for X being Subset of (Open_Domains_Lattice T) st X = F holds
( ( X <> {} implies "/\" (X,(Open_Domains_Lattice T)) = Int (meet F) ) & ( X = {} implies "/\" (X,(Open_Domains_Lattice T)) = [#] T ) )
let F be Subset-Family of T; ::_thesis: ( F is open-domains-family implies for X being Subset of (Open_Domains_Lattice T) st X = F holds
( ( X <> {} implies "/\" (X,(Open_Domains_Lattice T)) = Int (meet F) ) & ( X = {} implies "/\" (X,(Open_Domains_Lattice T)) = [#] T ) ) )
assume A1: F is open-domains-family ; ::_thesis: for X being Subset of (Open_Domains_Lattice T) st X = F holds
( ( X <> {} implies "/\" (X,(Open_Domains_Lattice T)) = Int (meet F) ) & ( X = {} implies "/\" (X,(Open_Domains_Lattice T)) = [#] T ) )
let X be Subset of (Open_Domains_Lattice T); ::_thesis: ( X = F implies ( ( X <> {} implies "/\" (X,(Open_Domains_Lattice T)) = Int (meet F) ) & ( X = {} implies "/\" (X,(Open_Domains_Lattice T)) = [#] T ) ) )
assume A2: X = F ; ::_thesis: ( ( X <> {} implies "/\" (X,(Open_Domains_Lattice T)) = Int (meet F) ) & ( X = {} implies "/\" (X,(Open_Domains_Lattice T)) = [#] T ) )
thus ( X <> {} implies "/\" (X,(Open_Domains_Lattice T)) = Int (meet F) ) ::_thesis: ( X = {} implies "/\" (X,(Open_Domains_Lattice T)) = [#] T )
proof
set A = Int (meet F);
Int (meet F) is open_condensed by A1, Th83;
then Int (meet F) in { C where C is Subset of T : C is open_condensed } ;
then A3: Int (meet F) in Open_Domains_of T by TDLAT_1:def_9;
then reconsider a = Int (meet F) as Element of (Open_Domains_Lattice T) by Th103;
A4: a is_less_than X
proof
let b be Element of (Open_Domains_Lattice T); :: according to LATTICE3:def_16 ::_thesis: ( not b in X or a [= b )
reconsider B = b as Element of Open_Domains_of T by Th103;
assume b in X ; ::_thesis: a [= b
then Int (meet F) c= B by A2, Th85;
hence a [= b by A3, Th106; ::_thesis: verum
end;
assume A5: X <> {} ; ::_thesis: "/\" (X,(Open_Domains_Lattice T)) = Int (meet F)
A6: for b being Element of (Open_Domains_Lattice T) st b is_less_than X holds
b [= a
proof
let b be Element of (Open_Domains_Lattice T); ::_thesis: ( b is_less_than X implies b [= a )
reconsider B = b as Element of Open_Domains_of T by Th103;
assume A7: b is_less_than X ; ::_thesis: b [= a
A8: for C being Subset of T st C in F holds
B c= C
proof
let C be Subset of T; ::_thesis: ( C in F implies B c= C )
reconsider C1 = C as Subset of T ;
assume A9: C in F ; ::_thesis: B c= C
then C1 is open_condensed by A1, Def4;
then C in { P where P is Subset of T : P is open_condensed } ;
then A10: C in Open_Domains_of T by TDLAT_1:def_9;
then reconsider c = C as Element of (Open_Domains_Lattice T) by Th103;
b [= c by A2, A7, A9, LATTICE3:def_16;
hence B c= C by A10, Th106; ::_thesis: verum
end;
B in Open_Domains_of T ;
then B in { C where C is Subset of T : C is open_condensed } by TDLAT_1:def_9;
then ex C being Subset of T st
( C = B & C is open_condensed ) ;
then B c= Int (meet F) by A2, A5, A8, Th85;
hence b [= a by A3, Th106; ::_thesis: verum
end;
Open_Domains_Lattice T is complete by Th108;
hence "/\" (X,(Open_Domains_Lattice T)) = Int (meet F) by A4, A6, LATTICE3:34; ::_thesis: verum
end;
thus ( X = {} implies "/\" (X,(Open_Domains_Lattice T)) = [#] T ) ::_thesis: verum
proof
set A = [#] T;
[#] T is open_condensed by TDLAT_1:21;
then [#] T in { C where C is Subset of T : C is open_condensed } ;
then A11: [#] T in Open_Domains_of T by TDLAT_1:def_9;
then reconsider a = [#] T as Element of (Open_Domains_Lattice T) by Th103;
A12: for b being Element of (Open_Domains_Lattice T) st b is_less_than X holds
b [= a
proof
let b be Element of (Open_Domains_Lattice T); ::_thesis: ( b is_less_than X implies b [= a )
reconsider B = b as Element of Open_Domains_of T by Th103;
assume b is_less_than X ; ::_thesis: b [= a
B c= [#] T ;
hence b [= a by A11, Th106; ::_thesis: verum
end;
assume A13: X = {} ; ::_thesis: "/\" (X,(Open_Domains_Lattice T)) = [#] T
A14: a is_less_than X
proof
let b be Element of (Open_Domains_Lattice T); :: according to LATTICE3:def_16 ::_thesis: ( not b in X or a [= b )
assume b in X ; ::_thesis: a [= b
hence a [= b by A13; ::_thesis: verum
end;
Open_Domains_Lattice T is complete by Th108;
hence "/\" (X,(Open_Domains_Lattice T)) = [#] T by A14, A12, LATTICE3:34; ::_thesis: verum
end;
end;
theorem :: TDLAT_2:111
for T being non empty TopSpace
for F being Subset-Family of T st F is open-domains-family holds
for X being Subset of (Domains_Lattice T) st X = F holds
"\/" (X,(Domains_Lattice T)) = Int (Cl (union F))
proof
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st F is open-domains-family holds
for X being Subset of (Domains_Lattice T) st X = F holds
"\/" (X,(Domains_Lattice T)) = Int (Cl (union F))
let F be Subset-Family of T; ::_thesis: ( F is open-domains-family implies for X being Subset of (Domains_Lattice T) st X = F holds
"\/" (X,(Domains_Lattice T)) = Int (Cl (union F)) )
A1: Int (union F) c= Int (Cl (union F)) by PRE_TOPC:18, TOPS_1:19;
assume A2: F is open-domains-family ; ::_thesis: for X being Subset of (Domains_Lattice T) st X = F holds
"\/" (X,(Domains_Lattice T)) = Int (Cl (union F))
then union F is open by Th81, TOPS_2:19;
then union F c= Int (Cl (union F)) by A1, TOPS_1:23;
then A3: (union F) \/ (Int (Cl (union F))) = Int (Cl (union F)) by XBOOLE_1:12;
let X be Subset of (Domains_Lattice T); ::_thesis: ( X = F implies "\/" (X,(Domains_Lattice T)) = Int (Cl (union F)) )
assume X = F ; ::_thesis: "\/" (X,(Domains_Lattice T)) = Int (Cl (union F))
hence "\/" (X,(Domains_Lattice T)) = Int (Cl (union F)) by A2, A3, Th80, Th92; ::_thesis: verum
end;