:: TOPS_3 semantic presentation
begin
theorem Th1: :: TOPS_3:1
for X being TopStruct
for A being Subset of X holds
( ( A = {} X implies A ` = [#] X ) & ( A ` = [#] X implies A = {} X ) & ( A = {} implies A ` = the carrier of X ) & ( A ` = the carrier of X implies A = {} ) )
proof
let X be TopStruct ; ::_thesis: for A being Subset of X holds
( ( A = {} X implies A ` = [#] X ) & ( A ` = [#] X implies A = {} X ) & ( A = {} implies A ` = the carrier of X ) & ( A ` = the carrier of X implies A = {} ) )
let A be Subset of X; ::_thesis: ( ( A = {} X implies A ` = [#] X ) & ( A ` = [#] X implies A = {} X ) & ( A = {} implies A ` = the carrier of X ) & ( A ` = the carrier of X implies A = {} ) )
thus ( A = {} X iff A ` = [#] X ) ::_thesis: ( A = {} iff A ` = the carrier of X )
proof
thus ( A = {} X implies A ` = [#] X ) ; ::_thesis: ( A ` = [#] X implies A = {} X )
assume A ` = [#] X ; ::_thesis: A = {} X
then (A `) ` = {} X by XBOOLE_1:37;
hence A = {} X ; ::_thesis: verum
end;
hence ( A = {} iff A ` = the carrier of X ) ; ::_thesis: verum
end;
theorem Th2: :: TOPS_3:2
for X being TopStruct
for A being Subset of X holds
( ( A = [#] X implies A ` = {} X ) & ( A ` = {} X implies A = [#] X ) & ( A = the carrier of X implies A ` = {} ) & ( A ` = {} implies A = the carrier of X ) )
proof
let X be TopStruct ; ::_thesis: for A being Subset of X holds
( ( A = [#] X implies A ` = {} X ) & ( A ` = {} X implies A = [#] X ) & ( A = the carrier of X implies A ` = {} ) & ( A ` = {} implies A = the carrier of X ) )
let A be Subset of X; ::_thesis: ( ( A = [#] X implies A ` = {} X ) & ( A ` = {} X implies A = [#] X ) & ( A = the carrier of X implies A ` = {} ) & ( A ` = {} implies A = the carrier of X ) )
thus ( A = [#] X iff A ` = {} X ) ::_thesis: ( A = the carrier of X iff A ` = {} )
proof
thus ( A = [#] X implies A ` = {} X ) by XBOOLE_1:37; ::_thesis: ( A ` = {} X implies A = [#] X )
assume A ` = {} X ; ::_thesis: A = [#] X
then (A `) ` = [#] X ;
hence A = [#] X ; ::_thesis: verum
end;
hence ( A = the carrier of X iff A ` = {} ) ; ::_thesis: verum
end;
theorem Th3: :: TOPS_3:3
for X being TopSpace
for A, B being Subset of X holds (Int A) /\ (Cl B) c= Cl (A /\ B)
proof
let X be TopSpace; ::_thesis: for A, B being Subset of X holds (Int A) /\ (Cl B) c= Cl (A /\ B)
let A, B be Subset of X; ::_thesis: (Int A) /\ (Cl B) c= Cl (A /\ B)
(Int A) /\ B c= A /\ B by TOPS_1:16, XBOOLE_1:26;
then A1: Cl ((Int A) /\ B) c= Cl (A /\ B) by PRE_TOPC:19;
(Int A) /\ (Cl B) c= Cl ((Int A) /\ B) by TOPS_1:13;
hence (Int A) /\ (Cl B) c= Cl (A /\ B) by A1, XBOOLE_1:1; ::_thesis: verum
end;
theorem Th4: :: TOPS_3:4
for X being TopSpace
for A, B being Subset of X holds Int (A \/ B) c= (Cl A) \/ (Int B)
proof
let X be TopSpace; ::_thesis: for A, B being Subset of X holds Int (A \/ B) c= (Cl A) \/ (Int B)
let A, B be Subset of X; ::_thesis: Int (A \/ B) c= (Cl A) \/ (Int B)
(Int (A `)) /\ (Cl (B `)) c= Cl ((A `) /\ (B `)) by Th3;
then (Cl ((A `) /\ (B `))) ` c= ((Int (A `)) /\ (Cl (B `))) ` by SUBSET_1:12;
then Int (((A `) /\ (B `)) `) c= ((Int (A `)) /\ (Cl (B `))) ` by TDLAT_3:3;
then Int (((A `) `) \/ ((B `) `)) c= ((Int (A `)) /\ (Cl (B `))) ` by XBOOLE_1:54;
then Int (A \/ B) c= ((Int (A `)) `) \/ ((Cl (B `)) `) by XBOOLE_1:54;
then Int (A \/ B) c= (Cl A) \/ ((Cl (B `)) `) by TDLAT_3:1;
hence Int (A \/ B) c= (Cl A) \/ (Int B) by TOPS_1:def_1; ::_thesis: verum
end;
theorem Th5: :: TOPS_3:5
for X being TopSpace
for B, A being Subset of X st A is closed holds
Int (A \/ B) c= A \/ (Int B)
proof
let X be TopSpace; ::_thesis: for B, A being Subset of X st A is closed holds
Int (A \/ B) c= A \/ (Int B)
let B, A be Subset of X; ::_thesis: ( A is closed implies Int (A \/ B) c= A \/ (Int B) )
assume A is closed ; ::_thesis: Int (A \/ B) c= A \/ (Int B)
then Cl A = A by PRE_TOPC:22;
hence Int (A \/ B) c= A \/ (Int B) by Th4; ::_thesis: verum
end;
theorem Th6: :: TOPS_3:6
for X being TopSpace
for B, A being Subset of X st A is closed holds
Int (A \/ B) = Int (A \/ (Int B))
proof
let X be TopSpace; ::_thesis: for B, A being Subset of X st A is closed holds
Int (A \/ B) = Int (A \/ (Int B))
let B, A be Subset of X; ::_thesis: ( A is closed implies Int (A \/ B) = Int (A \/ (Int B)) )
A \/ (Int B) c= A \/ B by TOPS_1:16, XBOOLE_1:9;
then A1: Int (A \/ (Int B)) c= Int (A \/ B) by TOPS_1:19;
assume A is closed ; ::_thesis: Int (A \/ B) = Int (A \/ (Int B))
then Int (Int (A \/ B)) c= Int (A \/ (Int B)) by Th5, TOPS_1:19;
hence Int (A \/ B) = Int (A \/ (Int B)) by A1, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th7: :: TOPS_3:7
for X being TopSpace
for A being Subset of X st A misses Int (Cl A) holds
Int (Cl A) = {}
proof
let X be TopSpace; ::_thesis: for A being Subset of X st A misses Int (Cl A) holds
Int (Cl A) = {}
let A be Subset of X; ::_thesis: ( A misses Int (Cl A) implies Int (Cl A) = {} )
reconsider A9 = A as Subset of X ;
assume A /\ (Int (Cl A)) = {} ; :: according to XBOOLE_0:def_7 ::_thesis: Int (Cl A) = {}
then A9 misses Int (Cl A9) by XBOOLE_0:def_7;
then Cl A misses Int (Cl A) by TSEP_1:36;
then (Cl A) /\ (Int (Cl A)) = {} by XBOOLE_0:def_7;
hence Int (Cl A) = {} by TOPS_1:16, XBOOLE_1:28; ::_thesis: verum
end;
theorem :: TOPS_3:8
for X being TopSpace
for A being Subset of X st A \/ (Cl (Int A)) = the carrier of X holds
Cl (Int A) = the carrier of X
proof
let X be TopSpace; ::_thesis: for A being Subset of X st A \/ (Cl (Int A)) = the carrier of X holds
Cl (Int A) = the carrier of X
let A be Subset of X; ::_thesis: ( A \/ (Cl (Int A)) = the carrier of X implies Cl (Int A) = the carrier of X )
assume A \/ (Cl (Int A)) = the carrier of X ; ::_thesis: Cl (Int A) = the carrier of X
then (Int A) \/ (Cl (Int A)) = the carrier of X by TDLAT_3:4;
hence Cl (Int A) = the carrier of X by PRE_TOPC:18, XBOOLE_1:12; ::_thesis: verum
end;
begin
definition
let X be TopStruct ;
let A be Subset of X;
redefine attr A is boundary means :Def1: :: TOPS_3:def 1
Int A = {} ;
compatibility
( A is boundary iff Int A = {} ) by TOPS_1:48;
end;
:: deftheorem Def1 defines boundary TOPS_3:def_1_:_
for X being TopStruct
for A being Subset of X holds
( A is boundary iff Int A = {} );
theorem :: TOPS_3:9
for X being TopSpace holds {} X is boundary ;
theorem Th10: :: TOPS_3:10
for X being non empty TopSpace
for A being Subset of X st A is boundary holds
A <> the carrier of X
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X st A is boundary holds
A <> the carrier of X
let A be Subset of X; ::_thesis: ( A is boundary implies A <> the carrier of X )
assume A1: Int A = {} ; :: according to TOPS_3:def_1 ::_thesis: A <> the carrier of X
assume A = the carrier of X ; ::_thesis: contradiction
then A = [#] X ;
hence contradiction by A1, TOPS_1:15; ::_thesis: verum
end;
theorem Th11: :: TOPS_3:11
for X being TopSpace
for B, A being Subset of X st B is boundary & A c= B holds
A is boundary
proof
let X be TopSpace; ::_thesis: for B, A being Subset of X st B is boundary & A c= B holds
A is boundary
let B, A be Subset of X; ::_thesis: ( B is boundary & A c= B implies A is boundary )
assume B is boundary ; ::_thesis: ( not A c= B or A is boundary )
then A1: Int B = {} ;
assume A c= B ; ::_thesis: A is boundary
then Int A = {} by A1, TOPS_1:19, XBOOLE_1:3;
hence A is boundary by TOPS_1:48; ::_thesis: verum
end;
theorem :: TOPS_3:12
for X being TopSpace
for A being Subset of X holds
( A is boundary iff for C being Subset of X st A ` c= C & C is closed holds
C = the carrier of X )
proof
let X be TopSpace; ::_thesis: for A being Subset of X holds
( A is boundary iff for C being Subset of X st A ` c= C & C is closed holds
C = the carrier of X )
let A be Subset of X; ::_thesis: ( A is boundary iff for C being Subset of X st A ` c= C & C is closed holds
C = the carrier of X )
thus ( A is boundary implies for C being Subset of X st A ` c= C & C is closed holds
C = the carrier of X ) ::_thesis: ( ( for C being Subset of X st A ` c= C & C is closed holds
C = the carrier of X ) implies A is boundary )
proof
assume A1: A is boundary ; ::_thesis: for C being Subset of X st A ` c= C & C is closed holds
C = the carrier of X
let C be Subset of X; ::_thesis: ( A ` c= C & C is closed implies C = the carrier of X )
assume A ` c= C ; ::_thesis: ( not C is closed or C = the carrier of X )
then A2: C ` c= (A `) ` by SUBSET_1:12;
assume C is closed ; ::_thesis: C = the carrier of X
then C ` = {} X by A1, A2, TOPS_1:50;
hence C = the carrier of X by Th2; ::_thesis: verum
end;
assume A3: for C being Subset of X st A ` c= C & C is closed holds
C = the carrier of X ; ::_thesis: A is boundary
now__::_thesis:_for_G_being_Subset_of_X_st_G_c=_A_&_G_is_open_holds_
G_=_{}
let G be Subset of X; ::_thesis: ( G c= A & G is open implies G = {} )
assume that
A4: G c= A and
A5: G is open ; ::_thesis: G = {}
A ` c= G ` by A4, SUBSET_1:12;
then G ` = the carrier of X by A3, A5;
hence G = {} by Th1; ::_thesis: verum
end;
hence A is boundary by TOPS_1:50; ::_thesis: verum
end;
theorem :: TOPS_3:13
for X being TopSpace
for A being Subset of X holds
( A is boundary iff for G being Subset of X st G <> {} & G is open holds
A ` meets G )
proof
let X be TopSpace; ::_thesis: for A being Subset of X holds
( A is boundary iff for G being Subset of X st G <> {} & G is open holds
A ` meets G )
let A be Subset of X; ::_thesis: ( A is boundary iff for G being Subset of X st G <> {} & G is open holds
A ` meets G )
thus ( A is boundary implies for G being Subset of X st G <> {} & G is open holds
A ` meets G ) ::_thesis: ( ( for G being Subset of X st G <> {} & G is open holds
A ` meets G ) implies A is boundary )
proof
assume A1: A is boundary ; ::_thesis: for G being Subset of X st G <> {} & G is open holds
A ` meets G
let G be Subset of X; ::_thesis: ( G <> {} & G is open implies A ` meets G )
assume A2: G <> {} ; ::_thesis: ( not G is open or A ` meets G )
assume A3: G is open ; ::_thesis: A ` meets G
assume A ` misses G ; ::_thesis: contradiction
then G c= A by SUBSET_1:24;
hence contradiction by A1, A2, A3, TOPS_1:50; ::_thesis: verum
end;
assume A4: for G being Subset of X st G <> {} & G is open holds
A ` meets G ; ::_thesis: A is boundary
assume Int A <> {} ; :: according to TOPS_3:def_1 ::_thesis: contradiction
then ( Int A c= A & A ` meets Int A ) by A4, TOPS_1:16;
hence contradiction by SUBSET_1:24; ::_thesis: verum
end;
theorem :: TOPS_3:14
for X being TopSpace
for A being Subset of X holds
( A is boundary iff for F being Subset of X st F is closed holds
Int F = Int (F \/ A) )
proof
let X be TopSpace; ::_thesis: for A being Subset of X holds
( A is boundary iff for F being Subset of X st F is closed holds
Int F = Int (F \/ A) )
let A be Subset of X; ::_thesis: ( A is boundary iff for F being Subset of X st F is closed holds
Int F = Int (F \/ A) )
thus ( A is boundary implies for F being Subset of X st F is closed holds
Int F = Int (F \/ A) ) ::_thesis: ( ( for F being Subset of X st F is closed holds
Int F = Int (F \/ A) ) implies A is boundary )
proof
assume A1: Int A = {} ; :: according to TOPS_3:def_1 ::_thesis: for F being Subset of X st F is closed holds
Int F = Int (F \/ A)
let F be Subset of X; ::_thesis: ( F is closed implies Int F = Int (F \/ A) )
assume F is closed ; ::_thesis: Int F = Int (F \/ A)
then Int (F \/ A) = Int (F \/ (Int A)) by Th6;
hence Int F = Int (F \/ A) by A1; ::_thesis: verum
end;
assume for F being Subset of X st F is closed holds
Int F = Int (F \/ A) ; ::_thesis: A is boundary
then Int ({} X) = Int (({} X) \/ A) ;
hence A is boundary by Def1; ::_thesis: verum
end;
theorem :: TOPS_3:15
for X being TopSpace
for A, B being Subset of X st A is boundary holds
A /\ B is boundary by Th11, XBOOLE_1:17;
definition
let X be TopStruct ;
let A be Subset of X;
redefine attr A is dense means :Def2: :: TOPS_3:def 2
Cl A = the carrier of X;
compatibility
( A is dense iff Cl A = the carrier of X )
proof
thus ( A is dense implies Cl A = the carrier of X ) ::_thesis: ( Cl A = the carrier of X implies A is dense )
proof
assume A is dense ; ::_thesis: Cl A = the carrier of X
then Cl A = [#] X by TOPS_1:def_3;
hence Cl A = the carrier of X ; ::_thesis: verum
end;
assume Cl A = the carrier of X ; ::_thesis: A is dense
then Cl A = [#] X ;
hence A is dense by TOPS_1:def_3; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines dense TOPS_3:def_2_:_
for X being TopStruct
for A being Subset of X holds
( A is dense iff Cl A = the carrier of X );
theorem :: TOPS_3:16
for X being TopSpace holds [#] X is dense ;
theorem Th17: :: TOPS_3:17
for X being non empty TopSpace
for A being Subset of X st A is dense holds
A <> {}
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X st A is dense holds
A <> {}
let A be Subset of X; ::_thesis: ( A is dense implies A <> {} )
assume A is dense ; ::_thesis: A <> {}
then A1: Cl A = [#] X by TOPS_1:def_3;
assume A = {} ; ::_thesis: contradiction
hence contradiction by A1, PRE_TOPC:22; ::_thesis: verum
end;
theorem Th18: :: TOPS_3:18
for X being non empty TopSpace
for A being Subset of X holds
( A is dense iff A ` is boundary )
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X holds
( A is dense iff A ` is boundary )
let A be Subset of X; ::_thesis: ( A is dense iff A ` is boundary )
thus ( A is dense implies A ` is boundary ) ::_thesis: ( A ` is boundary implies A is dense )
proof
assume A is dense ; ::_thesis: A ` is boundary
then (A `) ` is dense ;
hence A ` is boundary by TOPS_1:def_4; ::_thesis: verum
end;
assume A ` is boundary ; ::_thesis: A is dense
then (A `) ` is dense by TOPS_1:def_4;
hence A is dense ; ::_thesis: verum
end;
theorem :: TOPS_3:19
for X being non empty TopSpace
for A being Subset of X holds
( A is dense iff for C being Subset of X st A c= C & C is closed holds
C = the carrier of X )
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X holds
( A is dense iff for C being Subset of X st A c= C & C is closed holds
C = the carrier of X )
let A be Subset of X; ::_thesis: ( A is dense iff for C being Subset of X st A c= C & C is closed holds
C = the carrier of X )
thus ( A is dense implies for C being Subset of X st A c= C & C is closed holds
C = the carrier of X ) ::_thesis: ( ( for C being Subset of X st A c= C & C is closed holds
C = the carrier of X ) implies A is dense )
proof
assume A1: Cl A = the carrier of X ; :: according to TOPS_3:def_2 ::_thesis: for C being Subset of X st A c= C & C is closed holds
C = the carrier of X
let C be Subset of X; ::_thesis: ( A c= C & C is closed implies C = the carrier of X )
assume ( A c= C & C is closed ) ; ::_thesis: C = the carrier of X
then Cl A c= C by TOPS_1:5;
hence C = the carrier of X by A1, XBOOLE_0:def_10; ::_thesis: verum
end;
assume for C being Subset of X st A c= C & C is closed holds
C = the carrier of X ; ::_thesis: A is dense
then Cl A = the carrier of X by PRE_TOPC:18;
hence A is dense by Def2; ::_thesis: verum
end;
theorem :: TOPS_3:20
for X being non empty TopSpace
for A being Subset of X holds
( A is dense iff for G being Subset of X st G is open holds
Cl G = Cl (G /\ A) )
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X holds
( A is dense iff for G being Subset of X st G is open holds
Cl G = Cl (G /\ A) )
let A be Subset of X; ::_thesis: ( A is dense iff for G being Subset of X st G is open holds
Cl G = Cl (G /\ A) )
thus ( A is dense implies for G being Subset of X st G is open holds
Cl G = Cl (G /\ A) ) ::_thesis: ( ( for G being Subset of X st G is open holds
Cl G = Cl (G /\ A) ) implies A is dense )
proof
assume A1: A is dense ; ::_thesis: for G being Subset of X st G is open holds
Cl G = Cl (G /\ A)
let G be Subset of X; ::_thesis: ( G is open implies Cl G = Cl (G /\ A) )
assume G is open ; ::_thesis: Cl G = Cl (G /\ A)
then A2: Cl (G /\ (Cl A)) = Cl (G /\ A) by TOPS_1:14;
G /\ ([#] X) = G by XBOOLE_1:28;
hence Cl G = Cl (G /\ A) by A1, A2, TOPS_1:def_3; ::_thesis: verum
end;
assume for G being Subset of X st G is open holds
Cl G = Cl (G /\ A) ; ::_thesis: A is dense
then Cl ([#] X) = Cl (([#] X) /\ A) ;
then A3: [#] X = Cl (([#] X) /\ A) by TOPS_1:2;
([#] X) /\ A = A by XBOOLE_1:28;
hence A is dense by A3, Def2; ::_thesis: verum
end;
theorem :: TOPS_3:21
for X being non empty TopSpace
for A, B being Subset of X st A is dense holds
A \/ B is dense by TOPS_1:44, XBOOLE_1:7;
definition
let X be TopStruct ;
let A be Subset of X;
redefine attr A is nowhere_dense means :Def3: :: TOPS_3:def 3
Int (Cl A) = {} ;
compatibility
( A is nowhere_dense iff Int (Cl A) = {} )
proof
thus ( A is nowhere_dense implies Int (Cl A) = {} ) ::_thesis: ( Int (Cl A) = {} implies A is nowhere_dense )
proof
assume A is nowhere_dense ; ::_thesis: Int (Cl A) = {}
then Cl A is boundary by TOPS_1:def_5;
hence Int (Cl A) = {} ; ::_thesis: verum
end;
assume Int (Cl A) = {} ; ::_thesis: A is nowhere_dense
then Cl A is boundary by Def1;
hence A is nowhere_dense by TOPS_1:def_5; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines nowhere_dense TOPS_3:def_3_:_
for X being TopStruct
for A being Subset of X holds
( A is nowhere_dense iff Int (Cl A) = {} );
theorem :: TOPS_3:22
for X being non empty TopSpace holds {} X is nowhere_dense ;
theorem :: TOPS_3:23
for X being non empty TopSpace
for A being Subset of X st A is nowhere_dense holds
A <> the carrier of X by Th10;
theorem :: TOPS_3:24
for X being non empty TopSpace
for A being Subset of X st A is nowhere_dense holds
Cl A is nowhere_dense
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X st A is nowhere_dense holds
Cl A is nowhere_dense
let A be Subset of X; ::_thesis: ( A is nowhere_dense implies Cl A is nowhere_dense )
assume A is nowhere_dense ; ::_thesis: Cl A is nowhere_dense
then Cl A is boundary by TOPS_1:def_5;
hence Cl A is nowhere_dense ; ::_thesis: verum
end;
theorem :: TOPS_3:25
for X being non empty TopSpace
for A being Subset of X st A is nowhere_dense holds
not A is dense
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X st A is nowhere_dense holds
not A is dense
let A be Subset of X; ::_thesis: ( A is nowhere_dense implies not A is dense )
assume A1: Int (Cl A) = {} ; :: according to TOPS_3:def_3 ::_thesis: not A is dense
assume A is dense ; ::_thesis: contradiction
then Cl A = [#] X by TOPS_1:def_3;
hence contradiction by A1, TOPS_1:15; ::_thesis: verum
end;
theorem Th26: :: TOPS_3:26
for X being non empty TopSpace
for B, A being Subset of X st B is nowhere_dense & A c= B holds
A is nowhere_dense
proof
let X be non empty TopSpace; ::_thesis: for B, A being Subset of X st B is nowhere_dense & A c= B holds
A is nowhere_dense
let B, A be Subset of X; ::_thesis: ( B is nowhere_dense & A c= B implies A is nowhere_dense )
assume B is nowhere_dense ; ::_thesis: ( not A c= B or A is nowhere_dense )
then A1: Cl B is boundary by TOPS_1:def_5;
assume A c= B ; ::_thesis: A is nowhere_dense
then Cl A is boundary by A1, Th11, PRE_TOPC:19;
hence A is nowhere_dense by TOPS_1:def_5; ::_thesis: verum
end;
theorem Th27: :: TOPS_3:27
for X being non empty TopSpace
for A being Subset of X holds
( A is nowhere_dense iff ex C being Subset of X st
( A c= C & C is closed & C is boundary ) )
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X holds
( A is nowhere_dense iff ex C being Subset of X st
( A c= C & C is closed & C is boundary ) )
let A be Subset of X; ::_thesis: ( A is nowhere_dense iff ex C being Subset of X st
( A c= C & C is closed & C is boundary ) )
thus ( A is nowhere_dense implies ex C being Subset of X st
( A c= C & C is closed & C is boundary ) ) ::_thesis: ( ex C being Subset of X st
( A c= C & C is closed & C is boundary ) implies A is nowhere_dense )
proof
assume A1: A is nowhere_dense ; ::_thesis: ex C being Subset of X st
( A c= C & C is closed & C is boundary )
take Cl A ; ::_thesis: ( A c= Cl A & Cl A is closed & Cl A is boundary )
thus ( A c= Cl A & Cl A is closed & Cl A is boundary ) by A1, PRE_TOPC:18, TOPS_1:def_5; ::_thesis: verum
end;
given C being Subset of X such that A2: ( A c= C & C is closed & C is boundary ) ; ::_thesis: A is nowhere_dense
Cl A is boundary by A2, Th11, TOPS_1:5;
hence A is nowhere_dense by TOPS_1:def_5; ::_thesis: verum
end;
theorem Th28: :: TOPS_3:28
for X being non empty TopSpace
for A being Subset of X holds
( A is nowhere_dense iff for G being Subset of X st G <> {} & G is open holds
ex H being Subset of X st
( H c= G & H <> {} & H is open & A misses H ) )
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X holds
( A is nowhere_dense iff for G being Subset of X st G <> {} & G is open holds
ex H being Subset of X st
( H c= G & H <> {} & H is open & A misses H ) )
let A be Subset of X; ::_thesis: ( A is nowhere_dense iff for G being Subset of X st G <> {} & G is open holds
ex H being Subset of X st
( H c= G & H <> {} & H is open & A misses H ) )
thus ( A is nowhere_dense implies for G being Subset of X st G <> {} & G is open holds
ex H being Subset of X st
( H c= G & H <> {} & H is open & A misses H ) ) ::_thesis: ( ( for G being Subset of X st G <> {} & G is open holds
ex H being Subset of X st
( H c= G & H <> {} & H is open & A misses H ) ) implies A is nowhere_dense )
proof
assume A is nowhere_dense ; ::_thesis: for G being Subset of X st G <> {} & G is open holds
ex H being Subset of X st
( H c= G & H <> {} & H is open & A misses H )
then A1: Cl A is boundary by TOPS_1:def_5;
let G be Subset of X; ::_thesis: ( G <> {} & G is open implies ex H being Subset of X st
( H c= G & H <> {} & H is open & A misses H ) )
assume ( G <> {} & G is open ) ; ::_thesis: ex H being Subset of X st
( H c= G & H <> {} & H is open & A misses H )
then consider H being Subset of X such that
A2: ( H c= G & H <> {} & H is open & Cl A misses H ) by A1, TOPS_1:51;
take H ; ::_thesis: ( H c= G & H <> {} & H is open & A misses H )
thus ( H c= G & H <> {} & H is open & A misses H ) by A2, PRE_TOPC:18, XBOOLE_1:63; ::_thesis: verum
end;
assume A3: for G being Subset of X st G <> {} & G is open holds
ex H being Subset of X st
( H c= G & H <> {} & H is open & A misses H ) ; ::_thesis: A is nowhere_dense
for G being Subset of X st G <> {} & G is open holds
ex H being Subset of X st
( H c= G & H <> {} & H is open & Cl A misses H )
proof
let G be Subset of X; ::_thesis: ( G <> {} & G is open implies ex H being Subset of X st
( H c= G & H <> {} & H is open & Cl A misses H ) )
assume ( G <> {} & G is open ) ; ::_thesis: ex H being Subset of X st
( H c= G & H <> {} & H is open & Cl A misses H )
then consider H being Subset of X such that
A4: ( H c= G & H <> {} & H is open & A misses H ) by A3;
take H ; ::_thesis: ( H c= G & H <> {} & H is open & Cl A misses H )
thus ( H c= G & H <> {} & H is open & Cl A misses H ) by A4, TSEP_1:36; ::_thesis: verum
end;
then Cl A is boundary by TOPS_1:51;
hence A is nowhere_dense by TOPS_1:def_5; ::_thesis: verum
end;
theorem :: TOPS_3:29
for X being non empty TopSpace
for A, B being Subset of X st A is nowhere_dense holds
A /\ B is nowhere_dense by Th26, XBOOLE_1:17;
theorem Th30: :: TOPS_3:30
for X being non empty TopSpace
for A, B being Subset of X st A is nowhere_dense & B is boundary holds
A \/ B is boundary
proof
let X be non empty TopSpace; ::_thesis: for A, B being Subset of X st A is nowhere_dense & B is boundary holds
A \/ B is boundary
let A, B be Subset of X; ::_thesis: ( A is nowhere_dense & B is boundary implies A \/ B is boundary )
assume A is nowhere_dense ; ::_thesis: ( not B is boundary or A \/ B is boundary )
then A1: Cl A is boundary by TOPS_1:def_5;
assume B is boundary ; ::_thesis: A \/ B is boundary
then ( A c= Cl A & B \/ (Cl A) is boundary ) by A1, PRE_TOPC:18, TOPS_1:49;
hence A \/ B is boundary by Th11, XBOOLE_1:9; ::_thesis: verum
end;
definition
let X be TopStruct ;
let A be Subset of X;
attrA is everywhere_dense means :Def4: :: TOPS_3:def 4
Cl (Int A) = [#] X;
end;
:: deftheorem Def4 defines everywhere_dense TOPS_3:def_4_:_
for X being TopStruct
for A being Subset of X holds
( A is everywhere_dense iff Cl (Int A) = [#] X );
definition
let X be TopStruct ;
let A be Subset of X;
redefine attr A is everywhere_dense means :: TOPS_3:def 5
Cl (Int A) = the carrier of X;
compatibility
( A is everywhere_dense iff Cl (Int A) = the carrier of X )
proof
thus ( A is everywhere_dense implies Cl (Int A) = the carrier of X ) ::_thesis: ( Cl (Int A) = the carrier of X implies A is everywhere_dense )
proof
assume A is everywhere_dense ; ::_thesis: Cl (Int A) = the carrier of X
then Cl (Int A) = [#] X by Def4;
hence Cl (Int A) = the carrier of X ; ::_thesis: verum
end;
assume Cl (Int A) = the carrier of X ; ::_thesis: A is everywhere_dense
then Cl (Int A) = [#] X ;
hence A is everywhere_dense by Def4; ::_thesis: verum
end;
end;
:: deftheorem defines everywhere_dense TOPS_3:def_5_:_
for X being TopStruct
for A being Subset of X holds
( A is everywhere_dense iff Cl (Int A) = the carrier of X );
theorem :: TOPS_3:31
for X being non empty TopSpace holds [#] X is everywhere_dense
proof
let X be non empty TopSpace; ::_thesis: [#] X is everywhere_dense
Int ([#] X) = [#] X by TOPS_1:15;
then Cl (Int ([#] X)) = [#] X by TOPS_1:2;
hence [#] X is everywhere_dense by Def4; ::_thesis: verum
end;
theorem Th32: :: TOPS_3:32
for X being non empty TopSpace
for A being Subset of X st A is everywhere_dense holds
Int A is everywhere_dense
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X st A is everywhere_dense holds
Int A is everywhere_dense
let A be Subset of X; ::_thesis: ( A is everywhere_dense implies Int A is everywhere_dense )
assume A is everywhere_dense ; ::_thesis: Int A is everywhere_dense
then Cl (Int (Int A)) = [#] X by Def4;
hence Int A is everywhere_dense by Def4; ::_thesis: verum
end;
theorem Th33: :: TOPS_3:33
for X being non empty TopSpace
for A being Subset of X st A is everywhere_dense holds
A is dense
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X st A is everywhere_dense holds
A is dense
let A be Subset of X; ::_thesis: ( A is everywhere_dense implies A is dense )
assume A is everywhere_dense ; ::_thesis: A is dense
then Cl (Int A) = [#] X by Def4;
then [#] X c= Cl A by PRE_TOPC:19, TOPS_1:16;
then Cl A = [#] X by XBOOLE_0:def_10;
hence A is dense by TOPS_1:def_3; ::_thesis: verum
end;
theorem :: TOPS_3:34
for X being non empty TopSpace
for A being Subset of X st A is everywhere_dense holds
A <> {} by Th17, Th33;
theorem Th35: :: TOPS_3:35
for X being non empty TopSpace
for A being Subset of X holds
( A is everywhere_dense iff Int A is dense )
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X holds
( A is everywhere_dense iff Int A is dense )
let A be Subset of X; ::_thesis: ( A is everywhere_dense iff Int A is dense )
thus ( A is everywhere_dense implies Int A is dense ) by Th32, Th33; ::_thesis: ( Int A is dense implies A is everywhere_dense )
assume Int A is dense ; ::_thesis: A is everywhere_dense
then Cl (Int A) = [#] X by TOPS_1:def_3;
hence A is everywhere_dense by Def4; ::_thesis: verum
end;
theorem Th36: :: TOPS_3:36
for X being non empty TopSpace
for A being Subset of X st A is open & A is dense holds
A is everywhere_dense
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X st A is open & A is dense holds
A is everywhere_dense
let A be Subset of X; ::_thesis: ( A is open & A is dense implies A is everywhere_dense )
assume A is open ; ::_thesis: ( not A is dense or A is everywhere_dense )
then A1: A = Int A by TOPS_1:23;
assume A is dense ; ::_thesis: A is everywhere_dense
hence A is everywhere_dense by A1, Th35; ::_thesis: verum
end;
theorem :: TOPS_3:37
for X being non empty TopSpace
for A being Subset of X st A is everywhere_dense holds
not A is boundary
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X st A is everywhere_dense holds
not A is boundary
let A be Subset of X; ::_thesis: ( A is everywhere_dense implies not A is boundary )
assume A is everywhere_dense ; ::_thesis: not A is boundary
then A1: Cl (Int A) = [#] X by Def4;
assume A is boundary ; ::_thesis: contradiction
hence contradiction by A1, PRE_TOPC:22; ::_thesis: verum
end;
theorem Th38: :: TOPS_3:38
for X being non empty TopSpace
for A, B being Subset of X st A is everywhere_dense & A c= B holds
B is everywhere_dense
proof
let X be non empty TopSpace; ::_thesis: for A, B being Subset of X st A is everywhere_dense & A c= B holds
B is everywhere_dense
let A, B be Subset of X; ::_thesis: ( A is everywhere_dense & A c= B implies B is everywhere_dense )
assume A is everywhere_dense ; ::_thesis: ( not A c= B or B is everywhere_dense )
then A1: Cl (Int A) = [#] X by Def4;
assume A c= B ; ::_thesis: B is everywhere_dense
then Int A c= Int B by TOPS_1:19;
then Cl (Int A) c= Cl (Int B) by PRE_TOPC:19;
then [#] X = Cl (Int B) by A1, XBOOLE_0:def_10;
hence B is everywhere_dense by Def4; ::_thesis: verum
end;
theorem Th39: :: TOPS_3:39
for X being non empty TopSpace
for A being Subset of X holds
( A is everywhere_dense iff A ` is nowhere_dense )
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X holds
( A is everywhere_dense iff A ` is nowhere_dense )
let A be Subset of X; ::_thesis: ( A is everywhere_dense iff A ` is nowhere_dense )
thus ( A is everywhere_dense implies A ` is nowhere_dense ) ::_thesis: ( A ` is nowhere_dense implies A is everywhere_dense )
proof
assume A is everywhere_dense ; ::_thesis: A ` is nowhere_dense
then Cl (Int A) = [#] X by Def4;
then (Cl (Int A)) ` = {} X by Th2;
then Int ((Int A) `) = {} X by TDLAT_3:3;
then Int (Cl (A `)) = {} by TDLAT_3:2;
then Cl (A `) is boundary by TOPS_1:48;
hence A ` is nowhere_dense by TOPS_1:def_5; ::_thesis: verum
end;
assume A ` is nowhere_dense ; ::_thesis: A is everywhere_dense
then Cl (A `) is boundary by TOPS_1:def_5;
then Int (Cl (A `)) = {} X ;
then Int ((Int A) `) = {} X by TDLAT_3:2;
then (Cl (Int A)) ` = {} X by TDLAT_3:3;
then Cl (Int A) = [#] X by Th2;
hence A is everywhere_dense by Def4; ::_thesis: verum
end;
theorem Th40: :: TOPS_3:40
for X being non empty TopSpace
for A being Subset of X holds
( A is nowhere_dense iff A ` is everywhere_dense )
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X holds
( A is nowhere_dense iff A ` is everywhere_dense )
let A be Subset of X; ::_thesis: ( A is nowhere_dense iff A ` is everywhere_dense )
thus ( A is nowhere_dense implies A ` is everywhere_dense ) ::_thesis: ( A ` is everywhere_dense implies A is nowhere_dense )
proof
assume A is nowhere_dense ; ::_thesis: A ` is everywhere_dense
then Cl A is boundary by TOPS_1:def_5;
then Int (Cl A) = {} X ;
then Int ((Int (A `)) `) = {} X by TDLAT_3:1;
then (Cl (Int (A `))) ` = {} X by TDLAT_3:3;
then Cl (Int (A `)) = [#] X by Th2;
hence A ` is everywhere_dense by Def4; ::_thesis: verum
end;
assume A ` is everywhere_dense ; ::_thesis: A is nowhere_dense
then Cl (Int (A `)) = [#] X by Def4;
then (Cl (Int (A `))) ` = {} X by Th2;
then Int ((Int (A `)) `) = {} X by TDLAT_3:3;
then Int (Cl A) = {} by TDLAT_3:1;
then Cl A is boundary by TOPS_1:48;
hence A is nowhere_dense by TOPS_1:def_5; ::_thesis: verum
end;
theorem Th41: :: TOPS_3:41
for X being non empty TopSpace
for A being Subset of X holds
( A is everywhere_dense iff ex C being Subset of X st
( C c= A & C is open & C is dense ) )
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X holds
( A is everywhere_dense iff ex C being Subset of X st
( C c= A & C is open & C is dense ) )
let A be Subset of X; ::_thesis: ( A is everywhere_dense iff ex C being Subset of X st
( C c= A & C is open & C is dense ) )
thus ( A is everywhere_dense implies ex C being Subset of X st
( C c= A & C is open & C is dense ) ) ::_thesis: ( ex C being Subset of X st
( C c= A & C is open & C is dense ) implies A is everywhere_dense )
proof
assume A1: A is everywhere_dense ; ::_thesis: ex C being Subset of X st
( C c= A & C is open & C is dense )
take Int A ; ::_thesis: ( Int A c= A & Int A is open & Int A is dense )
thus ( Int A c= A & Int A is open & Int A is dense ) by A1, Th35, TOPS_1:16; ::_thesis: verum
end;
given C being Subset of X such that A2: ( C c= A & C is open & C is dense ) ; ::_thesis: A is everywhere_dense
Int A is dense by A2, TOPS_1:24, TOPS_1:44;
hence A is everywhere_dense by Th35; ::_thesis: verum
end;
theorem :: TOPS_3:42
for X being non empty TopSpace
for A being Subset of X holds
( A is everywhere_dense iff for F being Subset of X st F <> the carrier of X & F is closed holds
ex H being Subset of X st
( F c= H & H <> the carrier of X & H is closed & A \/ H = the carrier of X ) )
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X holds
( A is everywhere_dense iff for F being Subset of X st F <> the carrier of X & F is closed holds
ex H being Subset of X st
( F c= H & H <> the carrier of X & H is closed & A \/ H = the carrier of X ) )
let A be Subset of X; ::_thesis: ( A is everywhere_dense iff for F being Subset of X st F <> the carrier of X & F is closed holds
ex H being Subset of X st
( F c= H & H <> the carrier of X & H is closed & A \/ H = the carrier of X ) )
thus ( A is everywhere_dense implies for F being Subset of X st F <> the carrier of X & F is closed holds
ex H being Subset of X st
( F c= H & H <> the carrier of X & H is closed & A \/ H = the carrier of X ) ) ::_thesis: ( ( for F being Subset of X st F <> the carrier of X & F is closed holds
ex H being Subset of X st
( F c= H & H <> the carrier of X & H is closed & A \/ H = the carrier of X ) ) implies A is everywhere_dense )
proof
assume A is everywhere_dense ; ::_thesis: for F being Subset of X st F <> the carrier of X & F is closed holds
ex H being Subset of X st
( F c= H & H <> the carrier of X & H is closed & A \/ H = the carrier of X )
then A1: A ` is nowhere_dense by Th39;
let F be Subset of X; ::_thesis: ( F <> the carrier of X & F is closed implies ex H being Subset of X st
( F c= H & H <> the carrier of X & H is closed & A \/ H = the carrier of X ) )
assume F <> the carrier of X ; ::_thesis: ( not F is closed or ex H being Subset of X st
( F c= H & H <> the carrier of X & H is closed & A \/ H = the carrier of X ) )
then A2: ([#] X) \ F <> {} by PRE_TOPC:4;
assume F is closed ; ::_thesis: ex H being Subset of X st
( F c= H & H <> the carrier of X & H is closed & A \/ H = the carrier of X )
then consider G being Subset of X such that
A3: G c= F ` and
A4: G <> {} and
A5: G is open and
A6: A ` misses G by A1, A2, Th28;
take H = G ` ; ::_thesis: ( F c= H & H <> the carrier of X & H is closed & A \/ H = the carrier of X )
(F `) ` c= H by A3, SUBSET_1:12;
hence F c= H ; ::_thesis: ( H <> the carrier of X & H is closed & A \/ H = the carrier of X )
H ` <> {} by A4;
then ([#] X) \ H <> {} ;
hence H <> the carrier of X by PRE_TOPC:4; ::_thesis: ( H is closed & A \/ H = the carrier of X )
thus H is closed by A5; ::_thesis: A \/ H = the carrier of X
(A `) /\ (H `) = {} by A6, XBOOLE_0:def_7;
then (A \/ H) ` = {} X by XBOOLE_1:53;
hence A \/ H = the carrier of X by Th2; ::_thesis: verum
end;
assume A7: for F being Subset of X st F <> the carrier of X & F is closed holds
ex H being Subset of X st
( F c= H & H <> the carrier of X & H is closed & A \/ H = the carrier of X ) ; ::_thesis: A is everywhere_dense
for G being Subset of X st G <> {} & G is open holds
ex H being Subset of X st
( H c= G & H <> {} & H is open & A ` misses H )
proof
let G be Subset of X; ::_thesis: ( G <> {} & G is open implies ex H being Subset of X st
( H c= G & H <> {} & H is open & A ` misses H ) )
assume G <> {} ; ::_thesis: ( not G is open or ex H being Subset of X st
( H c= G & H <> {} & H is open & A ` misses H ) )
then (G `) ` <> {} ;
then A8: G ` <> [#] X by PRE_TOPC:4;
assume G is open ; ::_thesis: ex H being Subset of X st
( H c= G & H <> {} & H is open & A ` misses H )
then consider F being Subset of X such that
A9: G ` c= F and
A10: F <> the carrier of X and
A11: F is closed and
A12: A \/ F = the carrier of X by A7, A8;
take H = F ` ; ::_thesis: ( H c= G & H <> {} & H is open & A ` misses H )
H c= (G `) ` by A9, SUBSET_1:12;
hence H c= G ; ::_thesis: ( H <> {} & H is open & A ` misses H )
F <> [#] X by A10;
hence H <> {} by PRE_TOPC:4; ::_thesis: ( H is open & A ` misses H )
thus H is open by A11; ::_thesis: A ` misses H
(A \/ F) ` = {} X by A12, Th2;
hence (A `) /\ H = {} by XBOOLE_1:53; :: according to XBOOLE_0:def_7 ::_thesis: verum
end;
then A ` is nowhere_dense by Th28;
hence A is everywhere_dense by Th39; ::_thesis: verum
end;
theorem :: TOPS_3:43
for X being non empty TopSpace
for A, B being Subset of X st A is everywhere_dense holds
A \/ B is everywhere_dense by Th38, XBOOLE_1:7;
theorem Th44: :: TOPS_3:44
for X being non empty TopSpace
for A, B being Subset of X st A is everywhere_dense & B is everywhere_dense holds
A /\ B is everywhere_dense
proof
let X be non empty TopSpace; ::_thesis: for A, B being Subset of X st A is everywhere_dense & B is everywhere_dense holds
A /\ B is everywhere_dense
let A, B be Subset of X; ::_thesis: ( A is everywhere_dense & B is everywhere_dense implies A /\ B is everywhere_dense )
assume ( A is everywhere_dense & B is everywhere_dense ) ; ::_thesis: A /\ B is everywhere_dense
then ( A ` is nowhere_dense & B ` is nowhere_dense ) by Th39;
then ( (A `) \/ (B `) = (A /\ B) ` & (A `) \/ (B `) is nowhere_dense ) by TOPS_1:53, XBOOLE_1:54;
hence A /\ B is everywhere_dense by Th39; ::_thesis: verum
end;
theorem Th45: :: TOPS_3:45
for X being non empty TopSpace
for A, B being Subset of X st A is everywhere_dense & B is dense holds
A /\ B is dense
proof
let X be non empty TopSpace; ::_thesis: for A, B being Subset of X st A is everywhere_dense & B is dense holds
A /\ B is dense
let A, B be Subset of X; ::_thesis: ( A is everywhere_dense & B is dense implies A /\ B is dense )
assume A is everywhere_dense ; ::_thesis: ( not B is dense or A /\ B is dense )
then A1: A ` is nowhere_dense by Th39;
assume B is dense ; ::_thesis: A /\ B is dense
then B ` is boundary by Th18;
then ( (A `) \/ (B `) = (A /\ B) ` & (A `) \/ (B `) is boundary ) by A1, Th30, XBOOLE_1:54;
hence A /\ B is dense by Th18; ::_thesis: verum
end;
theorem :: TOPS_3:46
for X being non empty TopSpace
for A, B being Subset of X st A is dense & B is nowhere_dense holds
A \ B is dense
proof
let X be non empty TopSpace; ::_thesis: for A, B being Subset of X st A is dense & B is nowhere_dense holds
A \ B is dense
let A, B be Subset of X; ::_thesis: ( A is dense & B is nowhere_dense implies A \ B is dense )
assume A1: A is dense ; ::_thesis: ( not B is nowhere_dense or A \ B is dense )
A2: A \ B = (B `) /\ A by SUBSET_1:13;
assume B is nowhere_dense ; ::_thesis: A \ B is dense
then B ` is everywhere_dense by Th40;
hence A \ B is dense by A1, A2, Th45; ::_thesis: verum
end;
theorem :: TOPS_3:47
for X being non empty TopSpace
for A, B being Subset of X st A is everywhere_dense & B is boundary holds
A \ B is dense
proof
let X be non empty TopSpace; ::_thesis: for A, B being Subset of X st A is everywhere_dense & B is boundary holds
A \ B is dense
let A, B be Subset of X; ::_thesis: ( A is everywhere_dense & B is boundary implies A \ B is dense )
assume A1: A is everywhere_dense ; ::_thesis: ( not B is boundary or A \ B is dense )
A2: A \ B = A /\ (B `) by SUBSET_1:13;
assume B is boundary ; ::_thesis: A \ B is dense
then B ` is dense by TOPS_1:def_4;
hence A \ B is dense by A1, A2, Th45; ::_thesis: verum
end;
theorem :: TOPS_3:48
for X being non empty TopSpace
for A, B being Subset of X st A is everywhere_dense & B is nowhere_dense holds
A \ B is everywhere_dense
proof
let X be non empty TopSpace; ::_thesis: for A, B being Subset of X st A is everywhere_dense & B is nowhere_dense holds
A \ B is everywhere_dense
let A, B be Subset of X; ::_thesis: ( A is everywhere_dense & B is nowhere_dense implies A \ B is everywhere_dense )
assume A1: A is everywhere_dense ; ::_thesis: ( not B is nowhere_dense or A \ B is everywhere_dense )
A2: A \ B = A /\ (B `) by SUBSET_1:13;
assume B is nowhere_dense ; ::_thesis: A \ B is everywhere_dense
then B ` is everywhere_dense by Th40;
hence A \ B is everywhere_dense by A1, A2, Th44; ::_thesis: verum
end;
theorem :: TOPS_3:49
for X being non empty TopSpace
for D being Subset of X st D is everywhere_dense holds
ex C, B being Subset of X st
( C is open & C is dense & B is nowhere_dense & C \/ B = D & C misses B )
proof
let X be non empty TopSpace; ::_thesis: for D being Subset of X st D is everywhere_dense holds
ex C, B being Subset of X st
( C is open & C is dense & B is nowhere_dense & C \/ B = D & C misses B )
let D be Subset of X; ::_thesis: ( D is everywhere_dense implies ex C, B being Subset of X st
( C is open & C is dense & B is nowhere_dense & C \/ B = D & C misses B ) )
assume D is everywhere_dense ; ::_thesis: ex C, B being Subset of X st
( C is open & C is dense & B is nowhere_dense & C \/ B = D & C misses B )
then consider C being Subset of X such that
A1: C c= D and
A2: ( C is open & C is dense ) by Th41;
take C ; ::_thesis: ex B being Subset of X st
( C is open & C is dense & B is nowhere_dense & C \/ B = D & C misses B )
take B = D \ C; ::_thesis: ( C is open & C is dense & B is nowhere_dense & C \/ B = D & C misses B )
thus ( C is open & C is dense ) by A2; ::_thesis: ( B is nowhere_dense & C \/ B = D & C misses B )
C is everywhere_dense by A2, Th36;
then C ` is nowhere_dense by Th39;
hence B is nowhere_dense by Th26, XBOOLE_1:33; ::_thesis: ( C \/ B = D & C misses B )
thus ( C \/ B = D & C misses B ) by A1, XBOOLE_1:45, XBOOLE_1:79; ::_thesis: verum
end;
theorem :: TOPS_3:50
for X being non empty TopSpace
for D being Subset of X st D is everywhere_dense holds
ex C, B being Subset of X st
( C is open & C is dense & B is closed & B is boundary & C \/ (D /\ B) = D & C misses B & C \/ B = the carrier of X )
proof
let X be non empty TopSpace; ::_thesis: for D being Subset of X st D is everywhere_dense holds
ex C, B being Subset of X st
( C is open & C is dense & B is closed & B is boundary & C \/ (D /\ B) = D & C misses B & C \/ B = the carrier of X )
let D be Subset of X; ::_thesis: ( D is everywhere_dense implies ex C, B being Subset of X st
( C is open & C is dense & B is closed & B is boundary & C \/ (D /\ B) = D & C misses B & C \/ B = the carrier of X ) )
assume D is everywhere_dense ; ::_thesis: ex C, B being Subset of X st
( C is open & C is dense & B is closed & B is boundary & C \/ (D /\ B) = D & C misses B & C \/ B = the carrier of X )
then consider C being Subset of X such that
A1: C c= D and
A2: ( C is open & C is dense ) by Th41;
take C ; ::_thesis: ex B being Subset of X st
( C is open & C is dense & B is closed & B is boundary & C \/ (D /\ B) = D & C misses B & C \/ B = the carrier of X )
take B = C ` ; ::_thesis: ( C is open & C is dense & B is closed & B is boundary & C \/ (D /\ B) = D & C misses B & C \/ B = the carrier of X )
thus ( C is open & C is dense & B is closed & B is boundary ) by A2, Th18; ::_thesis: ( C \/ (D /\ B) = D & C misses B & C \/ B = the carrier of X )
thus C \/ (D /\ B) = (C \/ D) /\ (C \/ (C `)) by XBOOLE_1:24
.= (C \/ D) /\ ([#] X) by PRE_TOPC:2
.= C \/ D by XBOOLE_1:28
.= D by A1, XBOOLE_1:12 ; ::_thesis: ( C misses B & C \/ B = the carrier of X )
C misses B by XBOOLE_1:79;
hence C /\ B = {} by XBOOLE_0:def_7; :: according to XBOOLE_0:def_7 ::_thesis: C \/ B = the carrier of X
C \/ B = [#] X by PRE_TOPC:2;
hence C \/ B = the carrier of X ; ::_thesis: verum
end;
theorem :: TOPS_3:51
for X being non empty TopSpace
for D being Subset of X st D is nowhere_dense holds
ex C, B being Subset of X st
( C is closed & C is boundary & B is everywhere_dense & C /\ B = D & C \/ B = the carrier of X )
proof
let X be non empty TopSpace; ::_thesis: for D being Subset of X st D is nowhere_dense holds
ex C, B being Subset of X st
( C is closed & C is boundary & B is everywhere_dense & C /\ B = D & C \/ B = the carrier of X )
let D be Subset of X; ::_thesis: ( D is nowhere_dense implies ex C, B being Subset of X st
( C is closed & C is boundary & B is everywhere_dense & C /\ B = D & C \/ B = the carrier of X ) )
assume D is nowhere_dense ; ::_thesis: ex C, B being Subset of X st
( C is closed & C is boundary & B is everywhere_dense & C /\ B = D & C \/ B = the carrier of X )
then consider C being Subset of X such that
A1: D c= C and
A2: ( C is closed & C is boundary ) by Th27;
take C ; ::_thesis: ex B being Subset of X st
( C is closed & C is boundary & B is everywhere_dense & C /\ B = D & C \/ B = the carrier of X )
take B = D \/ (C `); ::_thesis: ( C is closed & C is boundary & B is everywhere_dense & C /\ B = D & C \/ B = the carrier of X )
thus ( C is closed & C is boundary ) by A2; ::_thesis: ( B is everywhere_dense & C /\ B = D & C \/ B = the carrier of X )
C ` is everywhere_dense by A2, Th40;
hence B is everywhere_dense by Th38, XBOOLE_1:7; ::_thesis: ( C /\ B = D & C \/ B = the carrier of X )
A3: C misses C ` by XBOOLE_1:79;
thus C /\ B = (C /\ D) \/ (C /\ (C `)) by XBOOLE_1:23
.= (C /\ D) \/ ({} X) by A3, XBOOLE_0:def_7
.= D by A1, XBOOLE_1:28 ; ::_thesis: C \/ B = the carrier of X
thus C \/ B = D \/ (C \/ (C `)) by XBOOLE_1:4
.= D \/ ([#] X) by PRE_TOPC:2
.= the carrier of X by XBOOLE_1:12 ; ::_thesis: verum
end;
theorem :: TOPS_3:52
for X being non empty TopSpace
for D being Subset of X st D is nowhere_dense holds
ex C, B being Subset of X st
( C is closed & C is boundary & B is open & B is dense & C /\ (D \/ B) = D & C misses B & C \/ B = the carrier of X )
proof
let X be non empty TopSpace; ::_thesis: for D being Subset of X st D is nowhere_dense holds
ex C, B being Subset of X st
( C is closed & C is boundary & B is open & B is dense & C /\ (D \/ B) = D & C misses B & C \/ B = the carrier of X )
let D be Subset of X; ::_thesis: ( D is nowhere_dense implies ex C, B being Subset of X st
( C is closed & C is boundary & B is open & B is dense & C /\ (D \/ B) = D & C misses B & C \/ B = the carrier of X ) )
assume D is nowhere_dense ; ::_thesis: ex C, B being Subset of X st
( C is closed & C is boundary & B is open & B is dense & C /\ (D \/ B) = D & C misses B & C \/ B = the carrier of X )
then consider C being Subset of X such that
A1: D c= C and
A2: ( C is closed & C is boundary ) by Th27;
take C ; ::_thesis: ex B being Subset of X st
( C is closed & C is boundary & B is open & B is dense & C /\ (D \/ B) = D & C misses B & C \/ B = the carrier of X )
take B = C ` ; ::_thesis: ( C is closed & C is boundary & B is open & B is dense & C /\ (D \/ B) = D & C misses B & C \/ B = the carrier of X )
thus ( C is closed & C is boundary & B is open & B is dense ) by A2; ::_thesis: ( C /\ (D \/ B) = D & C misses B & C \/ B = the carrier of X )
A3: C misses C ` by XBOOLE_1:79;
thus C /\ (D \/ B) = (C /\ D) \/ (C /\ (C `)) by XBOOLE_1:23
.= (C /\ D) \/ ({} X) by A3, XBOOLE_0:def_7
.= D by A1, XBOOLE_1:28 ; ::_thesis: ( C misses B & C \/ B = the carrier of X )
C misses B by XBOOLE_1:79;
hence C /\ B = {} by XBOOLE_0:def_7; :: according to XBOOLE_0:def_7 ::_thesis: C \/ B = the carrier of X
C \/ B = [#] X by PRE_TOPC:2;
hence C \/ B = the carrier of X ; ::_thesis: verum
end;
begin
theorem Th53: :: TOPS_3:53
for X being non empty TopSpace
for Y0 being SubSpace of X
for A being Subset of X
for B being Subset of Y0 st B c= A holds
Cl B c= Cl A
proof
let X be non empty TopSpace; ::_thesis: for Y0 being SubSpace of X
for A being Subset of X
for B being Subset of Y0 st B c= A holds
Cl B c= Cl A
let Y0 be SubSpace of X; ::_thesis: for A being Subset of X
for B being Subset of Y0 st B c= A holds
Cl B c= Cl A
let A be Subset of X; ::_thesis: for B being Subset of Y0 st B c= A holds
Cl B c= Cl A
let B be Subset of Y0; ::_thesis: ( B c= A implies Cl B c= Cl A )
assume A1: B c= A ; ::_thesis: Cl B c= Cl A
then reconsider D = B as Subset of X by XBOOLE_1:1;
Cl B = (Cl D) /\ ([#] Y0) by PRE_TOPC:17;
then A2: Cl B c= Cl D by XBOOLE_1:17;
Cl D c= Cl A by A1, PRE_TOPC:19;
hence Cl B c= Cl A by A2, XBOOLE_1:1; ::_thesis: verum
end;
theorem Th54: :: TOPS_3:54
for X being non empty TopSpace
for Y0 being SubSpace of X
for C, A being Subset of X
for B being Subset of Y0 st C is closed & C c= the carrier of Y0 & A c= C & A = B holds
Cl A = Cl B
proof
let X be non empty TopSpace; ::_thesis: for Y0 being SubSpace of X
for C, A being Subset of X
for B being Subset of Y0 st C is closed & C c= the carrier of Y0 & A c= C & A = B holds
Cl A = Cl B
let Y0 be SubSpace of X; ::_thesis: for C, A being Subset of X
for B being Subset of Y0 st C is closed & C c= the carrier of Y0 & A c= C & A = B holds
Cl A = Cl B
let C, A be Subset of X; ::_thesis: for B being Subset of Y0 st C is closed & C c= the carrier of Y0 & A c= C & A = B holds
Cl A = Cl B
let B be Subset of Y0; ::_thesis: ( C is closed & C c= the carrier of Y0 & A c= C & A = B implies Cl A = Cl B )
assume A1: C is closed ; ::_thesis: ( not C c= the carrier of Y0 or not A c= C or not A = B or Cl A = Cl B )
assume A2: C c= the carrier of Y0 ; ::_thesis: ( not A c= C or not A = B or Cl A = Cl B )
assume A c= C ; ::_thesis: ( not A = B or Cl A = Cl B )
then Cl A c= Cl C by PRE_TOPC:19;
then Cl A c= C by A1, PRE_TOPC:22;
then A3: Cl A = (Cl A) /\ ([#] Y0) by A2, XBOOLE_1:1, XBOOLE_1:28;
assume A = B ; ::_thesis: Cl A = Cl B
hence Cl A = Cl B by A3, PRE_TOPC:17; ::_thesis: verum
end;
theorem :: TOPS_3:55
for X being non empty TopSpace
for Y0 being non empty closed SubSpace of X
for A being Subset of X
for B being Subset of Y0 st A = B holds
Cl A = Cl B
proof
let X be non empty TopSpace; ::_thesis: for Y0 being non empty closed SubSpace of X
for A being Subset of X
for B being Subset of Y0 st A = B holds
Cl A = Cl B
let Y0 be non empty closed SubSpace of X; ::_thesis: for A being Subset of X
for B being Subset of Y0 st A = B holds
Cl A = Cl B
reconsider C = the carrier of Y0 as Subset of X by TSEP_1:1;
let A be Subset of X; ::_thesis: for B being Subset of Y0 st A = B holds
Cl A = Cl B
let B be Subset of Y0; ::_thesis: ( A = B implies Cl A = Cl B )
A1: C is closed by TSEP_1:11;
assume A = B ; ::_thesis: Cl A = Cl B
hence Cl A = Cl B by A1, Th54; ::_thesis: verum
end;
theorem Th56: :: TOPS_3:56
for X being non empty TopSpace
for Y0 being SubSpace of X
for A being Subset of X
for B being Subset of Y0 st A c= B holds
Int A c= Int B
proof
let X be non empty TopSpace; ::_thesis: for Y0 being SubSpace of X
for A being Subset of X
for B being Subset of Y0 st A c= B holds
Int A c= Int B
let Y0 be SubSpace of X; ::_thesis: for A being Subset of X
for B being Subset of Y0 st A c= B holds
Int A c= Int B
let A be Subset of X; ::_thesis: for B being Subset of Y0 st A c= B holds
Int A c= Int B
let B be Subset of Y0; ::_thesis: ( A c= B implies Int A c= Int B )
A1: Int A c= A by TOPS_1:16;
assume A c= B ; ::_thesis: Int A c= Int B
then A2: Int A c= B by A1, XBOOLE_1:1;
then reconsider C = Int A as Subset of Y0 by XBOOLE_1:1;
C is open by TOPS_2:25;
hence Int A c= Int B by A2, TOPS_1:24; ::_thesis: verum
end;
theorem Th57: :: TOPS_3:57
for X being non empty TopSpace
for Y0 being non empty SubSpace of X
for C, A being Subset of X
for B being Subset of Y0 st C is open & C c= the carrier of Y0 & A c= C & A = B holds
Int A = Int B
proof
let X be non empty TopSpace; ::_thesis: for Y0 being non empty SubSpace of X
for C, A being Subset of X
for B being Subset of Y0 st C is open & C c= the carrier of Y0 & A c= C & A = B holds
Int A = Int B
let Y0 be non empty SubSpace of X; ::_thesis: for C, A being Subset of X
for B being Subset of Y0 st C is open & C c= the carrier of Y0 & A c= C & A = B holds
Int A = Int B
let C, A be Subset of X; ::_thesis: for B being Subset of Y0 st C is open & C c= the carrier of Y0 & A c= C & A = B holds
Int A = Int B
let B be Subset of Y0; ::_thesis: ( C is open & C c= the carrier of Y0 & A c= C & A = B implies Int A = Int B )
assume A1: C is open ; ::_thesis: ( not C c= the carrier of Y0 or not A c= C or not A = B or Int A = Int B )
assume A2: C c= the carrier of Y0 ; ::_thesis: ( not A c= C or not A = B or Int A = Int B )
assume A3: A c= C ; ::_thesis: ( not A = B or Int A = Int B )
assume A4: A = B ; ::_thesis: Int A = Int B
A5: Int B c= B by TOPS_1:16;
then reconsider D = Int B as Subset of X by A4, XBOOLE_1:1;
Int B c= C by A3, A4, A5, XBOOLE_1:1;
then D is open by A1, A2, TSEP_1:9;
then A6: D c= Int A by A4, TOPS_1:16, TOPS_1:24;
Int A c= Int B by A4, Th56;
hence Int A = Int B by A6, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: TOPS_3:58
for X being non empty TopSpace
for Y0 being non empty open SubSpace of X
for A being Subset of X
for B being Subset of Y0 st A = B holds
Int A = Int B
proof
let X be non empty TopSpace; ::_thesis: for Y0 being non empty open SubSpace of X
for A being Subset of X
for B being Subset of Y0 st A = B holds
Int A = Int B
let Y0 be non empty open SubSpace of X; ::_thesis: for A being Subset of X
for B being Subset of Y0 st A = B holds
Int A = Int B
reconsider C = the carrier of Y0 as Subset of X by TSEP_1:1;
let A be Subset of X; ::_thesis: for B being Subset of Y0 st A = B holds
Int A = Int B
let B be Subset of Y0; ::_thesis: ( A = B implies Int A = Int B )
A1: C is open by TSEP_1:16;
assume A = B ; ::_thesis: Int A = Int B
hence Int A = Int B by A1, Th57; ::_thesis: verum
end;
theorem Th59: :: TOPS_3:59
for X being non empty TopSpace
for X0 being SubSpace of X
for A being Subset of X
for B being Subset of X0 st A c= B & A is dense holds
B is dense
proof
let X be non empty TopSpace; ::_thesis: for X0 being SubSpace of X
for A being Subset of X
for B being Subset of X0 st A c= B & A is dense holds
B is dense
let X0 be SubSpace of X; ::_thesis: for A being Subset of X
for B being Subset of X0 st A c= B & A is dense holds
B is dense
let A be Subset of X; ::_thesis: for B being Subset of X0 st A c= B & A is dense holds
B is dense
let B be Subset of X0; ::_thesis: ( A c= B & A is dense implies B is dense )
A1: [#] X0 c= [#] X by PRE_TOPC:def_4;
assume A2: A c= B ; ::_thesis: ( not A is dense or B is dense )
then reconsider C = A as Subset of X0 by XBOOLE_1:1;
assume A is dense ; ::_thesis: B is dense
then Cl A = [#] X by TOPS_1:def_3;
then [#] X0 = (Cl A) /\ ([#] X0) by A1, XBOOLE_1:28;
then Cl C = [#] X0 by PRE_TOPC:17;
then C is dense by TOPS_1:def_3;
hence B is dense by A2, TOPS_1:44; ::_thesis: verum
end;
theorem Th60: :: TOPS_3:60
for X being non empty TopSpace
for X0 being SubSpace of X
for C, A being Subset of X
for B being Subset of X0 st C c= the carrier of X0 & A c= C & A = B holds
( ( C is dense & B is dense ) iff A is dense )
proof
let X be non empty TopSpace; ::_thesis: for X0 being SubSpace of X
for C, A being Subset of X
for B being Subset of X0 st C c= the carrier of X0 & A c= C & A = B holds
( ( C is dense & B is dense ) iff A is dense )
let X0 be SubSpace of X; ::_thesis: for C, A being Subset of X
for B being Subset of X0 st C c= the carrier of X0 & A c= C & A = B holds
( ( C is dense & B is dense ) iff A is dense )
let C, A be Subset of X; ::_thesis: for B being Subset of X0 st C c= the carrier of X0 & A c= C & A = B holds
( ( C is dense & B is dense ) iff A is dense )
let B be Subset of X0; ::_thesis: ( C c= the carrier of X0 & A c= C & A = B implies ( ( C is dense & B is dense ) iff A is dense ) )
assume A1: C c= the carrier of X0 ; ::_thesis: ( not A c= C or not A = B or ( ( C is dense & B is dense ) iff A is dense ) )
reconsider P = the carrier of X0 as Subset of X by TSEP_1:1;
assume A2: A c= C ; ::_thesis: ( not A = B or ( ( C is dense & B is dense ) iff A is dense ) )
assume A3: A = B ; ::_thesis: ( ( C is dense & B is dense ) iff A is dense )
thus ( C is dense & B is dense implies A is dense ) ::_thesis: ( A is dense implies ( C is dense & B is dense ) )
proof
assume C is dense ; ::_thesis: ( not B is dense or A is dense )
then Cl C = [#] X by TOPS_1:def_3;
then A4: [#] X c= Cl P by A1, PRE_TOPC:19;
assume B is dense ; ::_thesis: A is dense
then Cl B = [#] X0 by TOPS_1:def_3;
then P = (Cl A) /\ ([#] X0) by A3, PRE_TOPC:17;
then Cl P c= Cl (Cl A) by PRE_TOPC:19, XBOOLE_1:17;
then [#] X c= Cl A by A4, XBOOLE_1:1;
then Cl A = [#] X by XBOOLE_0:def_10;
hence A is dense by TOPS_1:def_3; ::_thesis: verum
end;
thus ( A is dense implies ( C is dense & B is dense ) ) by A2, A3, Th59, TOPS_1:44; ::_thesis: verum
end;
theorem Th61: :: TOPS_3:61
for X being non empty TopSpace
for X0 being non empty SubSpace of X
for A being Subset of X
for B being Subset of X0 st A c= B & A is everywhere_dense holds
B is everywhere_dense
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty SubSpace of X
for A being Subset of X
for B being Subset of X0 st A c= B & A is everywhere_dense holds
B is everywhere_dense
let X0 be non empty SubSpace of X; ::_thesis: for A being Subset of X
for B being Subset of X0 st A c= B & A is everywhere_dense holds
B is everywhere_dense
let A be Subset of X; ::_thesis: for B being Subset of X0 st A c= B & A is everywhere_dense holds
B is everywhere_dense
let B be Subset of X0; ::_thesis: ( A c= B & A is everywhere_dense implies B is everywhere_dense )
assume A1: A c= B ; ::_thesis: ( not A is everywhere_dense or B is everywhere_dense )
then reconsider C = A as Subset of X0 by XBOOLE_1:1;
assume A is everywhere_dense ; ::_thesis: B is everywhere_dense
then Int A is dense by Th35;
then Int C is dense by Th56, Th59;
then Int B is dense by A1, TOPS_1:19, TOPS_1:44;
hence B is everywhere_dense by Th35; ::_thesis: verum
end;
theorem Th62: :: TOPS_3:62
for X being non empty TopSpace
for X0 being non empty SubSpace of X
for C, A being Subset of X
for B being Subset of X0 st C is open & C c= the carrier of X0 & A c= C & A = B holds
( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense )
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty SubSpace of X
for C, A being Subset of X
for B being Subset of X0 st C is open & C c= the carrier of X0 & A c= C & A = B holds
( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense )
let X0 be non empty SubSpace of X; ::_thesis: for C, A being Subset of X
for B being Subset of X0 st C is open & C c= the carrier of X0 & A c= C & A = B holds
( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense )
let C, A be Subset of X; ::_thesis: for B being Subset of X0 st C is open & C c= the carrier of X0 & A c= C & A = B holds
( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense )
let B be Subset of X0; ::_thesis: ( C is open & C c= the carrier of X0 & A c= C & A = B implies ( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense ) )
assume A1: C is open ; ::_thesis: ( not C c= the carrier of X0 or not A c= C or not A = B or ( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense ) )
assume C c= the carrier of X0 ; ::_thesis: ( not A c= C or not A = B or ( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense ) )
then reconsider E = C as Subset of X0 ;
A2: E is open by A1, TOPS_2:25;
assume A3: A c= C ; ::_thesis: ( not A = B or ( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense ) )
assume A4: A = B ; ::_thesis: ( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense )
A5: Int B c= B by TOPS_1:16;
then reconsider D = Int B as Subset of X by A4, XBOOLE_1:1;
Int B c= Int E by A3, A4, TOPS_1:19;
then A6: Int B c= E by A2, TOPS_1:23;
then A7: D is open by A1, TSEP_1:9;
thus ( C is dense & B is everywhere_dense implies A is everywhere_dense ) ::_thesis: ( A is everywhere_dense implies ( C is dense & B is everywhere_dense ) )
proof
assume A8: C is dense ; ::_thesis: ( not B is everywhere_dense or A is everywhere_dense )
assume B is everywhere_dense ; ::_thesis: A is everywhere_dense
then Int B is dense by Th35;
then D is dense by A6, A8, Th60;
then Int A is dense by A4, A5, A7, TOPS_1:24, TOPS_1:44;
hence A is everywhere_dense by Th35; ::_thesis: verum
end;
thus ( A is everywhere_dense implies ( C is dense & B is everywhere_dense ) ) ::_thesis: verum
proof
assume A9: A is everywhere_dense ; ::_thesis: ( C is dense & B is everywhere_dense )
hence C is dense by A3, Th33, Th38; ::_thesis: B is everywhere_dense
thus B is everywhere_dense by A4, A9, Th61; ::_thesis: verum
end;
end;
theorem :: TOPS_3:63
for X being non empty TopSpace
for X0 being non empty open SubSpace of X
for A, C being Subset of X
for B being Subset of X0 st C = the carrier of X0 & A = B holds
( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense )
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty open SubSpace of X
for A, C being Subset of X
for B being Subset of X0 st C = the carrier of X0 & A = B holds
( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense )
let X0 be non empty open SubSpace of X; ::_thesis: for A, C being Subset of X
for B being Subset of X0 st C = the carrier of X0 & A = B holds
( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense )
let A, C be Subset of X; ::_thesis: for B being Subset of X0 st C = the carrier of X0 & A = B holds
( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense )
let B be Subset of X0; ::_thesis: ( C = the carrier of X0 & A = B implies ( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense ) )
assume A1: C = the carrier of X0 ; ::_thesis: ( not A = B or ( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense ) )
assume A2: A = B ; ::_thesis: ( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense )
C is open by A1, TSEP_1:def_1;
hence ( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense ) by A1, A2, Th62; ::_thesis: verum
end;
theorem :: TOPS_3:64
for X being non empty TopSpace
for X0 being non empty SubSpace of X
for C, A being Subset of X
for B being Subset of X0 st C c= the carrier of X0 & A c= C & A = B holds
( ( C is everywhere_dense & B is everywhere_dense ) iff A is everywhere_dense )
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty SubSpace of X
for C, A being Subset of X
for B being Subset of X0 st C c= the carrier of X0 & A c= C & A = B holds
( ( C is everywhere_dense & B is everywhere_dense ) iff A is everywhere_dense )
let X0 be non empty SubSpace of X; ::_thesis: for C, A being Subset of X
for B being Subset of X0 st C c= the carrier of X0 & A c= C & A = B holds
( ( C is everywhere_dense & B is everywhere_dense ) iff A is everywhere_dense )
let C, A be Subset of X; ::_thesis: for B being Subset of X0 st C c= the carrier of X0 & A c= C & A = B holds
( ( C is everywhere_dense & B is everywhere_dense ) iff A is everywhere_dense )
let B be Subset of X0; ::_thesis: ( C c= the carrier of X0 & A c= C & A = B implies ( ( C is everywhere_dense & B is everywhere_dense ) iff A is everywhere_dense ) )
assume A1: C c= the carrier of X0 ; ::_thesis: ( not A c= C or not A = B or ( ( C is everywhere_dense & B is everywhere_dense ) iff A is everywhere_dense ) )
assume A2: A c= C ; ::_thesis: ( not A = B or ( ( C is everywhere_dense & B is everywhere_dense ) iff A is everywhere_dense ) )
assume A3: A = B ; ::_thesis: ( ( C is everywhere_dense & B is everywhere_dense ) iff A is everywhere_dense )
thus ( C is everywhere_dense & B is everywhere_dense implies A is everywhere_dense ) ::_thesis: ( A is everywhere_dense implies ( C is everywhere_dense & B is everywhere_dense ) )
proof
Int C c= C by TOPS_1:16;
then reconsider D = Int C as Subset of X0 by A1, XBOOLE_1:1;
A4: D /\ B c= Int C by XBOOLE_1:17;
then reconsider E = D /\ B as Subset of X by XBOOLE_1:1;
assume A5: C is everywhere_dense ; ::_thesis: ( not B is everywhere_dense or A is everywhere_dense )
then Int C is everywhere_dense by Th32;
then A6: D is everywhere_dense by Th61;
assume B is everywhere_dense ; ::_thesis: A is everywhere_dense
then A7: D /\ B is everywhere_dense by A6, Th44;
Int C is dense by A5, Th32, Th33;
then E is everywhere_dense by A7, A4, Th62;
hence A is everywhere_dense by A3, Th38, XBOOLE_1:17; ::_thesis: verum
end;
thus ( A is everywhere_dense implies ( C is everywhere_dense & B is everywhere_dense ) ) by A2, A3, Th38, Th61; ::_thesis: verum
end;
theorem Th65: :: TOPS_3:65
for X being non empty TopSpace
for X0 being non empty SubSpace of X
for A being Subset of X
for B being Subset of X0 st A c= B & B is boundary holds
A is boundary
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty SubSpace of X
for A being Subset of X
for B being Subset of X0 st A c= B & B is boundary holds
A is boundary
let X0 be non empty SubSpace of X; ::_thesis: for A being Subset of X
for B being Subset of X0 st A c= B & B is boundary holds
A is boundary
let A be Subset of X; ::_thesis: for B being Subset of X0 st A c= B & B is boundary holds
A is boundary
let B be Subset of X0; ::_thesis: ( A c= B & B is boundary implies A is boundary )
assume A1: A c= B ; ::_thesis: ( not B is boundary or A is boundary )
then reconsider C = A as Subset of X0 by XBOOLE_1:1;
assume Int B = {} ; :: according to TOPS_3:def_1 ::_thesis: A is boundary
then Int C = {} by A1, TOPS_1:19, XBOOLE_1:3;
then Int A = {} by Th56, XBOOLE_1:3;
hence A is boundary by Def1; ::_thesis: verum
end;
theorem Th66: :: TOPS_3:66
for X being non empty TopSpace
for X0 being non empty SubSpace of X
for C, A being Subset of X
for B being Subset of X0 st C is open & C c= the carrier of X0 & A c= C & A = B & A is boundary holds
B is boundary
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty SubSpace of X
for C, A being Subset of X
for B being Subset of X0 st C is open & C c= the carrier of X0 & A c= C & A = B & A is boundary holds
B is boundary
let X0 be non empty SubSpace of X; ::_thesis: for C, A being Subset of X
for B being Subset of X0 st C is open & C c= the carrier of X0 & A c= C & A = B & A is boundary holds
B is boundary
let C, A be Subset of X; ::_thesis: for B being Subset of X0 st C is open & C c= the carrier of X0 & A c= C & A = B & A is boundary holds
B is boundary
let B be Subset of X0; ::_thesis: ( C is open & C c= the carrier of X0 & A c= C & A = B & A is boundary implies B is boundary )
assume ( C is open & C c= the carrier of X0 & A c= C & A = B ) ; ::_thesis: ( not A is boundary or B is boundary )
then A1: Int A = Int B by Th57;
assume A is boundary ; ::_thesis: B is boundary
then Int A = {} ;
hence B is boundary by A1, TOPS_1:48; ::_thesis: verum
end;
theorem :: TOPS_3:67
for X being non empty TopSpace
for X0 being non empty open SubSpace of X
for A being Subset of X
for B being Subset of X0 st A = B holds
( A is boundary iff B is boundary )
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty open SubSpace of X
for A being Subset of X
for B being Subset of X0 st A = B holds
( A is boundary iff B is boundary )
let X0 be non empty open SubSpace of X; ::_thesis: for A being Subset of X
for B being Subset of X0 st A = B holds
( A is boundary iff B is boundary )
let A be Subset of X; ::_thesis: for B being Subset of X0 st A = B holds
( A is boundary iff B is boundary )
let B be Subset of X0; ::_thesis: ( A = B implies ( A is boundary iff B is boundary ) )
reconsider C = the carrier of X0 as Subset of X by TSEP_1:1;
A1: C is open by TSEP_1:def_1;
assume A = B ; ::_thesis: ( A is boundary iff B is boundary )
hence ( A is boundary iff B is boundary ) by A1, Th65, Th66; ::_thesis: verum
end;
theorem Th68: :: TOPS_3:68
for X being non empty TopSpace
for X0 being non empty SubSpace of X
for A being Subset of X
for B being Subset of X0 st A c= B & B is nowhere_dense holds
A is nowhere_dense
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty SubSpace of X
for A being Subset of X
for B being Subset of X0 st A c= B & B is nowhere_dense holds
A is nowhere_dense
let X0 be non empty SubSpace of X; ::_thesis: for A being Subset of X
for B being Subset of X0 st A c= B & B is nowhere_dense holds
A is nowhere_dense
let A be Subset of X; ::_thesis: for B being Subset of X0 st A c= B & B is nowhere_dense holds
A is nowhere_dense
let B be Subset of X0; ::_thesis: ( A c= B & B is nowhere_dense implies A is nowhere_dense )
reconsider D = the carrier of X0 as Subset of X by TSEP_1:1;
reconsider G = (Int (Cl A)) /\ ([#] X0) as Subset of X0 ;
assume A1: A c= B ; ::_thesis: ( not B is nowhere_dense or A is nowhere_dense )
then reconsider C = A as Subset of X0 by XBOOLE_1:1;
assume B is nowhere_dense ; ::_thesis: A is nowhere_dense
then C is nowhere_dense by A1, Th26;
then A2: ( G is open & Int (Cl C) = {} ) by Def3, TOPS_2:24;
(Int (Cl A)) /\ ([#] X0) c= (Cl A) /\ ([#] X0) by TOPS_1:16, XBOOLE_1:26;
then A3: (Int (Cl A)) /\ ([#] X0) c= Cl C by PRE_TOPC:17;
now__::_thesis:_not_Int_(Cl_A)_<>_{}
assume Int (Cl A) <> {} ; ::_thesis: contradiction
then A meets Int (Cl A) by Th7;
then A4: A /\ (Int (Cl A)) <> {} by XBOOLE_0:def_7;
C c= D ;
then (Int (Cl A)) /\ D <> {} by A4, XBOOLE_1:3, XBOOLE_1:26;
hence contradiction by A3, A2, TOPS_1:24, XBOOLE_1:3; ::_thesis: verum
end;
hence A is nowhere_dense by Def3; ::_thesis: verum
end;
Lm1: for X being non empty TopSpace
for X0 being non empty SubSpace of X
for C, A being Subset of X
for B being Subset of X0 st C is open & C = the carrier of X0 & A = B & A is nowhere_dense holds
B is nowhere_dense
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty SubSpace of X
for C, A being Subset of X
for B being Subset of X0 st C is open & C = the carrier of X0 & A = B & A is nowhere_dense holds
B is nowhere_dense
let X0 be non empty SubSpace of X; ::_thesis: for C, A being Subset of X
for B being Subset of X0 st C is open & C = the carrier of X0 & A = B & A is nowhere_dense holds
B is nowhere_dense
let C, A be Subset of X; ::_thesis: for B being Subset of X0 st C is open & C = the carrier of X0 & A = B & A is nowhere_dense holds
B is nowhere_dense
let B be Subset of X0; ::_thesis: ( C is open & C = the carrier of X0 & A = B & A is nowhere_dense implies B is nowhere_dense )
assume A1: C is open ; ::_thesis: ( not C = the carrier of X0 or not A = B or not A is nowhere_dense or B is nowhere_dense )
assume A2: C = the carrier of X0 ; ::_thesis: ( not A = B or not A is nowhere_dense or B is nowhere_dense )
assume A = B ; ::_thesis: ( not A is nowhere_dense or B is nowhere_dense )
then A3: Cl B c= Cl A by Th53;
then reconsider D = Cl B as Subset of X by XBOOLE_1:1;
assume A is nowhere_dense ; ::_thesis: B is nowhere_dense
then A4: Int (Cl A) = {} by Def3;
Int D = Int (Cl B) by A1, A2, Th57;
then Int (Cl B) = {} by A3, A4, TOPS_1:19, XBOOLE_1:3;
hence B is nowhere_dense by Def3; ::_thesis: verum
end;
theorem Th69: :: TOPS_3:69
for X being non empty TopSpace
for X0 being non empty SubSpace of X
for C, A being Subset of X
for B being Subset of X0 st C is open & C c= the carrier of X0 & A c= C & A = B & A is nowhere_dense holds
B is nowhere_dense
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty SubSpace of X
for C, A being Subset of X
for B being Subset of X0 st C is open & C c= the carrier of X0 & A c= C & A = B & A is nowhere_dense holds
B is nowhere_dense
let X0 be non empty SubSpace of X; ::_thesis: for C, A being Subset of X
for B being Subset of X0 st C is open & C c= the carrier of X0 & A c= C & A = B & A is nowhere_dense holds
B is nowhere_dense
let C, A be Subset of X; ::_thesis: for B being Subset of X0 st C is open & C c= the carrier of X0 & A c= C & A = B & A is nowhere_dense holds
B is nowhere_dense
let B be Subset of X0; ::_thesis: ( C is open & C c= the carrier of X0 & A c= C & A = B & A is nowhere_dense implies B is nowhere_dense )
assume A1: C is open ; ::_thesis: ( not C c= the carrier of X0 or not A c= C or not A = B or not A is nowhere_dense or B is nowhere_dense )
assume A2: C c= the carrier of X0 ; ::_thesis: ( not A c= C or not A = B or not A is nowhere_dense or B is nowhere_dense )
assume that
A3: A c= C and
A4: A = B ; ::_thesis: ( not A is nowhere_dense or B is nowhere_dense )
assume A5: A is nowhere_dense ; ::_thesis: B is nowhere_dense
A6: now__::_thesis:_(_C_<>_{}_implies_B_is_nowhere_dense_)
assume C <> {} ; ::_thesis: B is nowhere_dense
then consider X1 being non empty strict SubSpace of X such that
A7: C = the carrier of X1 by TSEP_1:10;
reconsider E = B as Subset of X1 by A3, A4, A7;
( E is nowhere_dense & X1 is SubSpace of X0 ) by A1, A2, A4, A5, A7, Lm1, TSEP_1:4;
hence B is nowhere_dense by Th68; ::_thesis: verum
end;
now__::_thesis:_(_C_=_{}_implies_B_is_nowhere_dense_)
assume C = {} ; ::_thesis: B is nowhere_dense
then B = {} X0 by A3, A4, XBOOLE_1:3;
hence B is nowhere_dense ; ::_thesis: verum
end;
hence B is nowhere_dense by A6; ::_thesis: verum
end;
theorem :: TOPS_3:70
for X being non empty TopSpace
for X0 being non empty open SubSpace of X
for A being Subset of X
for B being Subset of X0 st A = B holds
( A is nowhere_dense iff B is nowhere_dense )
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty open SubSpace of X
for A being Subset of X
for B being Subset of X0 st A = B holds
( A is nowhere_dense iff B is nowhere_dense )
let X0 be non empty open SubSpace of X; ::_thesis: for A being Subset of X
for B being Subset of X0 st A = B holds
( A is nowhere_dense iff B is nowhere_dense )
let A be Subset of X; ::_thesis: for B being Subset of X0 st A = B holds
( A is nowhere_dense iff B is nowhere_dense )
let B be Subset of X0; ::_thesis: ( A = B implies ( A is nowhere_dense iff B is nowhere_dense ) )
reconsider C = the carrier of X0 as Subset of X by TSEP_1:1;
A1: C is open by TSEP_1:def_1;
assume A = B ; ::_thesis: ( A is nowhere_dense iff B is nowhere_dense )
hence ( A is nowhere_dense iff B is nowhere_dense ) by A1, Th68, Th69; ::_thesis: verum
end;
begin
theorem :: TOPS_3:71
for X1, X2 being 1-sorted st the carrier of X1 = the carrier of X2 holds
for C1 being Subset of X1
for C2 being Subset of X2 holds
( C1 = C2 iff C1 ` = C2 ` )
proof
let X1, X2 be 1-sorted ; ::_thesis: ( the carrier of X1 = the carrier of X2 implies for C1 being Subset of X1
for C2 being Subset of X2 holds
( C1 = C2 iff C1 ` = C2 ` ) )
assume A1: the carrier of X1 = the carrier of X2 ; ::_thesis: for C1 being Subset of X1
for C2 being Subset of X2 holds
( C1 = C2 iff C1 ` = C2 ` )
let C1 be Subset of X1; ::_thesis: for C2 being Subset of X2 holds
( C1 = C2 iff C1 ` = C2 ` )
let C2 be Subset of X2; ::_thesis: ( C1 = C2 iff C1 ` = C2 ` )
thus ( C1 = C2 implies C1 ` = C2 ` ) by A1; ::_thesis: ( C1 ` = C2 ` implies C1 = C2 )
thus ( C1 ` = C2 ` implies C1 = C2 ) ::_thesis: verum
proof
assume C1 ` = C2 ` ; ::_thesis: C1 = C2
hence C1 = ([#] X2) \ (C2 `) by A1, PRE_TOPC:3
.= C2 by PRE_TOPC:3 ;
::_thesis: verum
end;
end;
theorem Th72: :: TOPS_3:72
for X1, X2 being TopStruct st the carrier of X1 = the carrier of X2 & ( for C1 being Subset of X1
for C2 being Subset of X2 st C1 = C2 holds
( C1 is open iff C2 is open ) ) holds
TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #)
proof
let X1, X2 be TopStruct ; ::_thesis: ( the carrier of X1 = the carrier of X2 & ( for C1 being Subset of X1
for C2 being Subset of X2 st C1 = C2 holds
( C1 is open iff C2 is open ) ) implies TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) )
assume A1: the carrier of X1 = the carrier of X2 ; ::_thesis: ( ex C1 being Subset of X1 ex C2 being Subset of X2 st
( C1 = C2 & not ( C1 is open iff C2 is open ) ) or TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) )
assume A2: for C1 being Subset of X1
for C2 being Subset of X2 st C1 = C2 holds
( C1 is open iff C2 is open ) ; ::_thesis: TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #)
now__::_thesis:_for_D_being_set_st_D_in_the_topology_of_X2_holds_
D_in_the_topology_of_X1
let D be set ; ::_thesis: ( D in the topology of X2 implies D in the topology of X1 )
assume A3: D in the topology of X2 ; ::_thesis: D in the topology of X1
then reconsider C2 = D as Subset of X2 ;
reconsider C1 = C2 as Subset of X1 by A1;
C2 is open by A3, PRE_TOPC:def_2;
then C1 is open by A2;
hence D in the topology of X1 by PRE_TOPC:def_2; ::_thesis: verum
end;
then A4: the topology of X2 c= the topology of X1 by TARSKI:def_3;
now__::_thesis:_for_D_being_set_st_D_in_the_topology_of_X1_holds_
D_in_the_topology_of_X2
let D be set ; ::_thesis: ( D in the topology of X1 implies D in the topology of X2 )
assume A5: D in the topology of X1 ; ::_thesis: D in the topology of X2
then reconsider C1 = D as Subset of X1 ;
reconsider C2 = C1 as Subset of X2 by A1;
C1 is open by A5, PRE_TOPC:def_2;
then C2 is open by A2;
hence D in the topology of X2 by PRE_TOPC:def_2; ::_thesis: verum
end;
then the topology of X1 c= the topology of X2 by TARSKI:def_3;
hence TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) by A1, A4, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th73: :: TOPS_3:73
for X1, X2 being TopStruct st the carrier of X1 = the carrier of X2 & ( for C1 being Subset of X1
for C2 being Subset of X2 st C1 = C2 holds
( C1 is closed iff C2 is closed ) ) holds
TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #)
proof
let X1, X2 be TopStruct ; ::_thesis: ( the carrier of X1 = the carrier of X2 & ( for C1 being Subset of X1
for C2 being Subset of X2 st C1 = C2 holds
( C1 is closed iff C2 is closed ) ) implies TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) )
assume A1: the carrier of X1 = the carrier of X2 ; ::_thesis: ( ex C1 being Subset of X1 ex C2 being Subset of X2 st
( C1 = C2 & not ( C1 is closed iff C2 is closed ) ) or TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) )
assume A2: for C1 being Subset of X1
for C2 being Subset of X2 st C1 = C2 holds
( C1 is closed iff C2 is closed ) ; ::_thesis: TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #)
now__::_thesis:_for_C1_being_Subset_of_X1
for_C2_being_Subset_of_X2_st_C1_=_C2_holds_
(_(_C1_is_open_implies_C2_is_open_)_&_(_C2_is_open_implies_C1_is_open_)_)
let C1 be Subset of X1; ::_thesis: for C2 being Subset of X2 st C1 = C2 holds
( ( C1 is open implies C2 is open ) & ( C2 is open implies C1 is open ) )
let C2 be Subset of X2; ::_thesis: ( C1 = C2 implies ( ( C1 is open implies C2 is open ) & ( C2 is open implies C1 is open ) ) )
assume A3: C1 = C2 ; ::_thesis: ( ( C1 is open implies C2 is open ) & ( C2 is open implies C1 is open ) )
thus ( C1 is open implies C2 is open ) ::_thesis: ( C2 is open implies C1 is open )
proof
assume C1 is open ; ::_thesis: C2 is open
then C1 ` is closed by TOPS_1:4;
then C2 ` is closed by A1, A2, A3;
hence C2 is open by TOPS_1:4; ::_thesis: verum
end;
thus ( C2 is open implies C1 is open ) ::_thesis: verum
proof
assume C2 is open ; ::_thesis: C1 is open
then C2 ` is closed by TOPS_1:4;
then C1 ` is closed by A1, A2, A3;
hence C1 is open by TOPS_1:4; ::_thesis: verum
end;
end;
hence TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) by A1, Th72; ::_thesis: verum
end;
theorem :: TOPS_3:74
for X1, X2 being TopSpace st the carrier of X1 = the carrier of X2 & ( for C1 being Subset of X1
for C2 being Subset of X2 st C1 = C2 holds
Int C1 = Int C2 ) holds
TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #)
proof
let X1, X2 be TopSpace; ::_thesis: ( the carrier of X1 = the carrier of X2 & ( for C1 being Subset of X1
for C2 being Subset of X2 st C1 = C2 holds
Int C1 = Int C2 ) implies TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) )
assume A1: the carrier of X1 = the carrier of X2 ; ::_thesis: ( ex C1 being Subset of X1 ex C2 being Subset of X2 st
( C1 = C2 & not Int C1 = Int C2 ) or TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) )
assume A2: for C1 being Subset of X1
for C2 being Subset of X2 st C1 = C2 holds
Int C1 = Int C2 ; ::_thesis: TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #)
now__::_thesis:_for_C1_being_Subset_of_X1
for_C2_being_Subset_of_X2_st_C1_=_C2_holds_
(_(_C1_is_open_implies_C2_is_open_)_&_(_C2_is_open_implies_C1_is_open_)_)
let C1 be Subset of X1; ::_thesis: for C2 being Subset of X2 st C1 = C2 holds
( ( C1 is open implies C2 is open ) & ( C2 is open implies C1 is open ) )
let C2 be Subset of X2; ::_thesis: ( C1 = C2 implies ( ( C1 is open implies C2 is open ) & ( C2 is open implies C1 is open ) ) )
assume A3: C1 = C2 ; ::_thesis: ( ( C1 is open implies C2 is open ) & ( C2 is open implies C1 is open ) )
thus ( C1 is open implies C2 is open ) ::_thesis: ( C2 is open implies C1 is open )
proof
assume C1 is open ; ::_thesis: C2 is open
then C1 = Int C1 by TOPS_1:23;
then C2 = Int C2 by A2, A3;
hence C2 is open ; ::_thesis: verum
end;
thus ( C2 is open implies C1 is open ) ::_thesis: verum
proof
assume C2 is open ; ::_thesis: C1 is open
then C2 = Int C2 by TOPS_1:23;
then C1 = Int C1 by A2, A3;
hence C1 is open ; ::_thesis: verum
end;
end;
hence TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) by A1, Th72; ::_thesis: verum
end;
theorem :: TOPS_3:75
for X1, X2 being TopSpace st the carrier of X1 = the carrier of X2 & ( for C1 being Subset of X1
for C2 being Subset of X2 st C1 = C2 holds
Cl C1 = Cl C2 ) holds
TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #)
proof
let X1, X2 be TopSpace; ::_thesis: ( the carrier of X1 = the carrier of X2 & ( for C1 being Subset of X1
for C2 being Subset of X2 st C1 = C2 holds
Cl C1 = Cl C2 ) implies TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) )
assume A1: the carrier of X1 = the carrier of X2 ; ::_thesis: ( ex C1 being Subset of X1 ex C2 being Subset of X2 st
( C1 = C2 & not Cl C1 = Cl C2 ) or TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) )
assume A2: for C1 being Subset of X1
for C2 being Subset of X2 st C1 = C2 holds
Cl C1 = Cl C2 ; ::_thesis: TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #)
now__::_thesis:_for_C1_being_Subset_of_X1
for_C2_being_Subset_of_X2_st_C1_=_C2_holds_
(_(_C1_is_closed_implies_C2_is_closed_)_&_(_C2_is_closed_implies_C1_is_closed_)_)
let C1 be Subset of X1; ::_thesis: for C2 being Subset of X2 st C1 = C2 holds
( ( C1 is closed implies C2 is closed ) & ( C2 is closed implies C1 is closed ) )
let C2 be Subset of X2; ::_thesis: ( C1 = C2 implies ( ( C1 is closed implies C2 is closed ) & ( C2 is closed implies C1 is closed ) ) )
assume A3: C1 = C2 ; ::_thesis: ( ( C1 is closed implies C2 is closed ) & ( C2 is closed implies C1 is closed ) )
thus ( C1 is closed implies C2 is closed ) ::_thesis: ( C2 is closed implies C1 is closed )
proof
assume C1 is closed ; ::_thesis: C2 is closed
then C1 = Cl C1 by PRE_TOPC:22;
then C2 = Cl C2 by A2, A3;
hence C2 is closed ; ::_thesis: verum
end;
thus ( C2 is closed implies C1 is closed ) ::_thesis: verum
proof
assume C2 is closed ; ::_thesis: C1 is closed
then C2 = Cl C2 by PRE_TOPC:22;
then C1 = Cl C1 by A2, A3;
hence C1 is closed ; ::_thesis: verum
end;
end;
hence TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) by A1, Th73; ::_thesis: verum
end;
theorem Th76: :: TOPS_3:76
for X1, X2 being TopSpace
for D1 being Subset of X1
for D2 being Subset of X2 st D1 = D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is open holds
D2 is open
proof
let X1, X2 be TopSpace; ::_thesis: for D1 being Subset of X1
for D2 being Subset of X2 st D1 = D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is open holds
D2 is open
let D1 be Subset of X1; ::_thesis: for D2 being Subset of X2 st D1 = D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is open holds
D2 is open
let D2 be Subset of X2; ::_thesis: ( D1 = D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is open implies D2 is open )
assume A1: D1 = D2 ; ::_thesis: ( not TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) or not D1 is open or D2 is open )
assume A2: TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) ; ::_thesis: ( not D1 is open or D2 is open )
assume D1 in the topology of X1 ; :: according to PRE_TOPC:def_2 ::_thesis: D2 is open
hence D2 is open by A1, A2, PRE_TOPC:def_2; ::_thesis: verum
end;
theorem Th77: :: TOPS_3:77
for X1, X2 being TopSpace
for D1 being Subset of X1
for D2 being Subset of X2 st D1 = D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) holds
Int D1 = Int D2
proof
let X1, X2 be TopSpace; ::_thesis: for D1 being Subset of X1
for D2 being Subset of X2 st D1 = D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) holds
Int D1 = Int D2
let D1 be Subset of X1; ::_thesis: for D2 being Subset of X2 st D1 = D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) holds
Int D1 = Int D2
let D2 be Subset of X2; ::_thesis: ( D1 = D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) implies Int D1 = Int D2 )
assume A1: D1 = D2 ; ::_thesis: ( not TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) or Int D1 = Int D2 )
A2: Int D1 c= D1 by TOPS_1:16;
then reconsider C2 = Int D1 as Subset of X2 by A1, XBOOLE_1:1;
assume A3: TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) ; ::_thesis: Int D1 = Int D2
then A4: C2 c= Int D2 by A1, A2, Th76, TOPS_1:24;
A5: Int D2 c= D2 by TOPS_1:16;
then reconsider C1 = Int D2 as Subset of X1 by A1, XBOOLE_1:1;
C1 c= Int D1 by A1, A3, A5, Th76, TOPS_1:24;
hence Int D1 = Int D2 by A4, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th78: :: TOPS_3:78
for X1, X2 being TopSpace
for D1 being Subset of X1
for D2 being Subset of X2 st D1 c= D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) holds
Int D1 c= Int D2
proof
let X1, X2 be TopSpace; ::_thesis: for D1 being Subset of X1
for D2 being Subset of X2 st D1 c= D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) holds
Int D1 c= Int D2
let D1 be Subset of X1; ::_thesis: for D2 being Subset of X2 st D1 c= D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) holds
Int D1 c= Int D2
let D2 be Subset of X2; ::_thesis: ( D1 c= D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) implies Int D1 c= Int D2 )
assume A1: D1 c= D2 ; ::_thesis: ( not TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) or Int D1 c= Int D2 )
then reconsider C2 = D1 as Subset of X2 by XBOOLE_1:1;
assume TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) ; ::_thesis: Int D1 c= Int D2
then Int D1 = Int C2 by Th77;
hence Int D1 c= Int D2 by A1, TOPS_1:19; ::_thesis: verum
end;
theorem Th79: :: TOPS_3:79
for X1, X2 being TopSpace
for D1 being Subset of X1
for D2 being Subset of X2 st D1 = D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is closed holds
D2 is closed
proof
let X1, X2 be TopSpace; ::_thesis: for D1 being Subset of X1
for D2 being Subset of X2 st D1 = D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is closed holds
D2 is closed
let D1 be Subset of X1; ::_thesis: for D2 being Subset of X2 st D1 = D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is closed holds
D2 is closed
let D2 be Subset of X2; ::_thesis: ( D1 = D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is closed implies D2 is closed )
assume A1: D1 = D2 ; ::_thesis: ( not TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) or not D1 is closed or D2 is closed )
assume A2: TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) ; ::_thesis: ( not D1 is closed or D2 is closed )
assume D1 is closed ; ::_thesis: D2 is closed
then D2 ` is open by A1, A2, Th76;
hence D2 is closed by TOPS_1:3; ::_thesis: verum
end;
theorem Th80: :: TOPS_3:80
for X1, X2 being TopSpace
for D1 being Subset of X1
for D2 being Subset of X2 st D1 = D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) holds
Cl D1 = Cl D2
proof
let X1, X2 be TopSpace; ::_thesis: for D1 being Subset of X1
for D2 being Subset of X2 st D1 = D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) holds
Cl D1 = Cl D2
let D1 be Subset of X1; ::_thesis: for D2 being Subset of X2 st D1 = D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) holds
Cl D1 = Cl D2
let D2 be Subset of X2; ::_thesis: ( D1 = D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) implies Cl D1 = Cl D2 )
assume A1: D1 = D2 ; ::_thesis: ( not TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) or Cl D1 = Cl D2 )
assume A2: TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) ; ::_thesis: Cl D1 = Cl D2
then reconsider C2 = Cl D1 as Subset of X2 ;
D1 c= Cl D1 by PRE_TOPC:18;
then A3: Cl D2 c= C2 by A1, A2, Th79, TOPS_1:5;
reconsider C1 = Cl D2 as Subset of X1 by A2;
D2 c= Cl D2 by PRE_TOPC:18;
then Cl D1 c= C1 by A1, A2, Th79, TOPS_1:5;
hence Cl D1 = Cl D2 by A3, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th81: :: TOPS_3:81
for X1, X2 being TopSpace
for D1 being Subset of X1
for D2 being Subset of X2 st D1 c= D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) holds
Cl D1 c= Cl D2
proof
let X1, X2 be TopSpace; ::_thesis: for D1 being Subset of X1
for D2 being Subset of X2 st D1 c= D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) holds
Cl D1 c= Cl D2
let D1 be Subset of X1; ::_thesis: for D2 being Subset of X2 st D1 c= D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) holds
Cl D1 c= Cl D2
let D2 be Subset of X2; ::_thesis: ( D1 c= D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) implies Cl D1 c= Cl D2 )
assume A1: D1 c= D2 ; ::_thesis: ( not TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) or Cl D1 c= Cl D2 )
assume A2: TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) ; ::_thesis: Cl D1 c= Cl D2
then reconsider C2 = D1 as Subset of X2 ;
Cl D1 = Cl C2 by A2, Th80;
hence Cl D1 c= Cl D2 by A1, PRE_TOPC:19; ::_thesis: verum
end;
theorem Th82: :: TOPS_3:82
for X1, X2 being TopSpace
for D1 being Subset of X1
for D2 being Subset of X2 st D2 c= D1 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is boundary holds
D2 is boundary
proof
let X1, X2 be TopSpace; ::_thesis: for D1 being Subset of X1
for D2 being Subset of X2 st D2 c= D1 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is boundary holds
D2 is boundary
let D1 be Subset of X1; ::_thesis: for D2 being Subset of X2 st D2 c= D1 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is boundary holds
D2 is boundary
let D2 be Subset of X2; ::_thesis: ( D2 c= D1 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is boundary implies D2 is boundary )
assume A1: D2 c= D1 ; ::_thesis: ( not TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) or not D1 is boundary or D2 is boundary )
then reconsider C1 = D2 as Subset of X1 by XBOOLE_1:1;
assume A2: TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) ; ::_thesis: ( not D1 is boundary or D2 is boundary )
assume D1 is boundary ; ::_thesis: D2 is boundary
then C1 is boundary by A1, Th11;
then A3: Int C1 = {} ;
Int C1 = Int D2 by A2, Th77;
hence D2 is boundary by A3, Def1; ::_thesis: verum
end;
theorem Th83: :: TOPS_3:83
for X1, X2 being TopSpace
for D1 being Subset of X1
for D2 being Subset of X2 st D1 c= D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is dense holds
D2 is dense
proof
let X1, X2 be TopSpace; ::_thesis: for D1 being Subset of X1
for D2 being Subset of X2 st D1 c= D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is dense holds
D2 is dense
let D1 be Subset of X1; ::_thesis: for D2 being Subset of X2 st D1 c= D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is dense holds
D2 is dense
let D2 be Subset of X2; ::_thesis: ( D1 c= D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is dense implies D2 is dense )
assume A1: D1 c= D2 ; ::_thesis: ( not TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) or not D1 is dense or D2 is dense )
then reconsider C2 = D1 as Subset of X2 by XBOOLE_1:1;
assume A2: TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) ; ::_thesis: ( not D1 is dense or D2 is dense )
assume D1 is dense ; ::_thesis: D2 is dense
then A3: Cl D1 = the carrier of X1 by Def2;
Cl D1 = Cl C2 by A2, Th80;
then C2 is dense by A2, A3, Def2;
hence D2 is dense by A1, TOPS_1:44; ::_thesis: verum
end;
theorem :: TOPS_3:84
for X1, X2 being TopSpace
for D1 being Subset of X1
for D2 being Subset of X2 st D2 c= D1 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is nowhere_dense holds
D2 is nowhere_dense
proof
let X1, X2 be TopSpace; ::_thesis: for D1 being Subset of X1
for D2 being Subset of X2 st D2 c= D1 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is nowhere_dense holds
D2 is nowhere_dense
let D1 be Subset of X1; ::_thesis: for D2 being Subset of X2 st D2 c= D1 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is nowhere_dense holds
D2 is nowhere_dense
let D2 be Subset of X2; ::_thesis: ( D2 c= D1 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is nowhere_dense implies D2 is nowhere_dense )
assume A1: D2 c= D1 ; ::_thesis: ( not TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) or not D1 is nowhere_dense or D2 is nowhere_dense )
assume A2: TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) ; ::_thesis: ( not D1 is nowhere_dense or D2 is nowhere_dense )
assume D1 is nowhere_dense ; ::_thesis: D2 is nowhere_dense
then Cl D1 is boundary by TOPS_1:def_5;
then Cl D2 is boundary by A1, A2, Th81, Th82;
hence D2 is nowhere_dense by TOPS_1:def_5; ::_thesis: verum
end;
theorem :: TOPS_3:85
for X1, X2 being non empty TopSpace
for D1 being Subset of X1
for D2 being Subset of X2 st D1 c= D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is everywhere_dense holds
D2 is everywhere_dense
proof
let X1, X2 be non empty TopSpace; ::_thesis: for D1 being Subset of X1
for D2 being Subset of X2 st D1 c= D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is everywhere_dense holds
D2 is everywhere_dense
let D1 be Subset of X1; ::_thesis: for D2 being Subset of X2 st D1 c= D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is everywhere_dense holds
D2 is everywhere_dense
let D2 be Subset of X2; ::_thesis: ( D1 c= D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is everywhere_dense implies D2 is everywhere_dense )
assume A1: D1 c= D2 ; ::_thesis: ( not TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) or not D1 is everywhere_dense or D2 is everywhere_dense )
assume A2: TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) ; ::_thesis: ( not D1 is everywhere_dense or D2 is everywhere_dense )
assume D1 is everywhere_dense ; ::_thesis: D2 is everywhere_dense
then Int D1 is dense by Th35;
then Int D2 is dense by A1, A2, Th78, Th83;
hence D2 is everywhere_dense by Th35; ::_thesis: verum
end;