:: TEX_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: TEX_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty TopSpace
for D, B being Subset of X
for C being Subset of (X modified_with_respect_to D) st B = C & B is open holds
C is open
proof end;

theorem :: TEX_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty TopSpace
for D, B being Subset of X
for C being Subset of (X modified_with_respect_to D) st B = C & B is closed holds
C is closed
proof end;

theorem Th3: :: TEX_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty TopSpace
for D being Subset of X
for C being Subset of (X modified_with_respect_to (D ` )) st C = D holds
C is closed
proof end;

theorem Th4: :: TEX_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty TopSpace
for D being Subset of X
for C being Subset of (X modified_with_respect_to D) st C = D & D is dense holds
( C is dense & C is open )
proof end;

theorem Th5: :: TEX_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty TopSpace
for D being Subset of X
for C being Subset of (X modified_with_respect_to D) st D c= C & D is dense holds
C is everywhere_dense
proof end;

theorem Th6: :: TEX_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty TopSpace
for D being Subset of X
for C being Subset of (X modified_with_respect_to (D ` )) st C = D & D is boundary holds
( C is boundary & C is closed )
proof end;

theorem Th7: :: TEX_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty TopSpace
for D being Subset of X
for C being Subset of (X modified_with_respect_to (D ` )) st C c= D & D is boundary holds
C is nowhere_dense
proof end;

Lm1: for X, Y being set holds
( X c= Y iff X is Subset of Y )
;

definition
let Y be non empty 1-sorted ;
redefine attr Y is trivial means :Def1: :: TEX_1:def 1
ex d being Element of Y st the carrier of Y = {d};
compatibility
( Y is trivial iff ex d being Element of Y st the carrier of Y = {d} )
proof end;
end;

:: deftheorem Def1 defines trivial TEX_1:def 1 :
for Y being non empty 1-sorted holds
( Y is trivial iff ex d being Element of Y st the carrier of Y = {d} );

registration
let A be non empty set ;
cluster 1-sorted(# A #) -> non empty ;
coherence
not 1-sorted(# A #) is empty
by STRUCT_0:def 1;
end;

registration
cluster strict non empty trivial 1-sorted ;
existence
ex b1 being 1-sorted st
( b1 is trivial & b1 is strict & not b1 is empty )
proof end;
cluster strict non empty non trivial 1-sorted ;
existence
ex b1 being 1-sorted st
( not b1 is trivial & b1 is strict & not b1 is empty )
proof end;
end;

registration
cluster non empty trivial strict TopStruct ;
existence
ex b1 being TopStruct st
( b1 is trivial & b1 is strict & not b1 is empty )
proof end;
cluster non empty non trivial strict TopStruct ;
existence
ex b1 being TopStruct st
( not b1 is trivial & b1 is strict & not b1 is empty )
proof end;
end;

theorem :: TEX_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being non empty trivial TopStruct st not the topology of Y is empty & Y is almost_discrete holds
Y is TopSpace-like
proof end;

registration
cluster non empty trivial strict TopStruct ;
existence
ex b1 being TopSpace st
( b1 is trivial & b1 is strict & not b1 is empty )
proof end;
end;

registration
cluster non empty trivial -> non empty discrete anti-discrete TopStruct ;
coherence
for b1 being non empty TopSpace st b1 is trivial holds
( b1 is anti-discrete & b1 is discrete )
proof end;
cluster non empty discrete anti-discrete -> non empty trivial TopStruct ;
coherence
for b1 being non empty TopSpace st b1 is discrete & b1 is anti-discrete holds
b1 is trivial
proof end;
end;

registration
cluster non empty non trivial strict TopStruct ;
existence
ex b1 being TopSpace st
( not b1 is trivial & b1 is strict & not b1 is empty )
proof end;
end;

registration
cluster non empty non discrete -> non empty non trivial TopStruct ;
coherence
for b1 being non empty TopSpace st not b1 is discrete holds
not b1 is trivial
proof end;
cluster non empty non anti-discrete -> non empty non trivial TopStruct ;
coherence
for b1 being non empty TopSpace st not b1 is anti-discrete holds
not b1 is trivial
proof end;
end;

definition
let D be set ;
func cobool D -> Subset-Family of D equals :: TEX_1:def 2
{{} ,D};
coherence
{{} ,D} is Subset-Family of D
proof end;
end;

:: deftheorem defines cobool TEX_1:def 2 :
for D being set holds cobool D = {{} ,D};

registration
let D be set ;
cluster cobool D -> non empty ;
coherence
not cobool D is empty
;
end;

definition
let D be set ;
func ADTS D -> TopStruct equals :: TEX_1:def 3
TopStruct(# D,(cobool D) #);
coherence
TopStruct(# D,(cobool D) #) is TopStruct
;
end;

:: deftheorem defines ADTS TEX_1:def 3 :
for D being set holds ADTS D = TopStruct(# D,(cobool D) #);

registration
let D be set ;
cluster ADTS D -> strict TopSpace-like anti-discrete ;
coherence
( ADTS D is strict & ADTS D is anti-discrete & ADTS D is TopSpace-like )
proof end;
end;

registration
let D be non empty set ;
cluster ADTS D -> non empty strict TopSpace-like anti-discrete ;
coherence
not ADTS D is empty
;
end;

theorem Th9: :: TEX_1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty anti-discrete TopSpace holds TopStruct(# the carrier of X,the topology of X #) = ADTS the carrier of X by TDLAT_3:def 2;

theorem :: TEX_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty TopSpace st TopStruct(# the carrier of X,the topology of X #) = TopStruct(# the carrier of (ADTS the carrier of X),the topology of (ADTS the carrier of X) #) holds
X is anti-discrete by TDLAT_3:def 2;

theorem Th11: :: TEX_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty anti-discrete TopSpace
for A being Subset of X holds
( ( A is empty implies Cl A = {} ) & ( not A is empty implies Cl A = the carrier of X ) )
proof end;

theorem Th12: :: TEX_1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty anti-discrete TopSpace
for A being Subset of X holds
( ( A <> the carrier of X implies Int A = {} ) & ( A = the carrier of X implies Int A = the carrier of X ) )
proof end;

theorem Th13: :: TEX_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty TopSpace st ( for A being Subset of X st not A is empty holds
Cl A = the carrier of X ) holds
X is anti-discrete
proof end;

theorem Th14: :: TEX_1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty TopSpace st ( for A being Subset of X st A <> the carrier of X holds
Int A = {} ) holds
X is anti-discrete
proof end;

theorem :: TEX_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty anti-discrete TopSpace
for A being Subset of X holds
( ( A <> {} implies A is dense ) & ( A <> the carrier of X implies A is boundary ) )
proof end;

theorem :: TEX_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty TopSpace st ( for A being Subset of X st A <> {} holds
A is dense ) holds
X is anti-discrete
proof end;

theorem :: TEX_1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty TopSpace st ( for A being Subset of X st A <> the carrier of X holds
A is boundary ) holds
X is anti-discrete
proof end;

registration
let D be set ;
cluster 1TopSp D -> discrete ;
coherence
1TopSp D is discrete
proof end;
end;

theorem Th18: :: TEX_1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty discrete TopSpace holds TopStruct(# the carrier of X,the topology of X #) = 1TopSp the carrier of X
proof end;

theorem :: TEX_1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty TopSpace st TopStruct(# the carrier of X,the topology of X #) = TopStruct(# the carrier of (1TopSp the carrier of X),the topology of (1TopSp the carrier of X) #) holds
X is discrete
proof end;

theorem :: TEX_1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty discrete TopSpace
for A being Subset of X holds
( Cl A = A & Int A = A )
proof end;

theorem :: TEX_1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty TopSpace st ( for A being Subset of X holds Cl A = A ) holds
X is discrete
proof end;

theorem :: TEX_1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty TopSpace st ( for A being Subset of X holds Int A = A ) holds
X is discrete
proof end;

theorem Th23: :: TEX_1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set holds
( ADTS D = 1TopSp D iff ex d0 being Element of D st D = {d0} )
proof end;

registration
cluster non empty non trivial strict discrete non anti-discrete TopStruct ;
existence
ex b1 being TopSpace st
( b1 is discrete & not b1 is anti-discrete & b1 is strict & not b1 is empty )
proof end;
cluster non empty non trivial strict non discrete anti-discrete TopStruct ;
existence
ex b1 being TopSpace st
( b1 is anti-discrete & not b1 is discrete & b1 is strict & not b1 is empty )
proof end;
end;

definition
let D be set ;
let F be Subset-Family of D;
let S be set ;
:: original: \
redefine func F \ S -> Subset-Family of D;
coherence
F \ S is Subset-Family of D
proof end;
end;

definition
let D be set ;
let d0 be Element of D;
canceled;
func STS D,d0 -> TopStruct equals :: TEX_1:def 5
TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #);
coherence
TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) is TopStruct
;
end;

:: deftheorem TEX_1:def 4 :
canceled;

:: deftheorem defines STS TEX_1:def 5 :
for D being set
for d0 being Element of D holds STS D,d0 = TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #);

registration
let D be set ;
let d0 be Element of D;
cluster STS D,d0 -> strict TopSpace-like ;
coherence
( STS D,d0 is strict & STS D,d0 is TopSpace-like )
proof end;
end;

registration
let D be non empty set ;
let d0 be Element of D;
cluster STS D,d0 -> non empty strict TopSpace-like ;
coherence
not STS D,d0 is empty
;
end;

theorem Th24: :: TEX_1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for d0 being Element of D
for A being Subset of (STS D,d0) holds
( ( {d0} c= A implies A is closed ) & ( not A is empty & A is closed implies {d0} c= A ) )
proof end;

theorem Th25: :: TEX_1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for d0 being Element of D st not D \ {d0} is empty holds
for A being Subset of (STS D,d0) holds
( ( A = {d0} implies ( A is closed & A is boundary ) ) & ( not A is empty & A is closed & A is boundary implies A = {d0} ) )
proof end;

theorem Th26: :: TEX_1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for d0 being Element of D
for A being Subset of (STS D,d0) holds
( ( A c= D \ {d0} implies A is open ) & ( A <> D & A is open implies A c= D \ {d0} ) )
proof end;

theorem :: TEX_1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for d0 being Element of D st not D \ {d0} is empty holds
for A being Subset of (STS D,d0) holds
( ( A = D \ {d0} implies ( A is open & A is dense ) ) & ( A <> D & A is open & A is dense implies A = D \ {d0} ) )
proof end;

registration
cluster non empty non trivial strict non discrete non anti-discrete TopStruct ;
existence
ex b1 being TopSpace st
( not b1 is anti-discrete & not b1 is discrete & b1 is strict & not b1 is empty )
proof end;
end;

theorem Th28: :: TEX_1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for d0 being Element of D
for Y being non empty TopSpace holds
( TopStruct(# the carrier of Y,the topology of Y #) = TopStruct(# the carrier of (STS D,d0),the topology of (STS D,d0) #) iff ( the carrier of Y = D & ( for A being Subset of Y holds
( ( {d0} c= A implies A is closed ) & ( not A is empty & A is closed implies {d0} c= A ) ) ) ) )
proof end;

theorem Th29: :: TEX_1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for d0 being Element of D
for Y being non empty TopSpace holds
( TopStruct(# the carrier of Y,the topology of Y #) = TopStruct(# the carrier of (STS D,d0),the topology of (STS D,d0) #) iff ( the carrier of Y = D & ( for A being Subset of Y holds
( ( A c= D \ {d0} implies A is open ) & ( A <> D & A is open implies A c= D \ {d0} ) ) ) ) )
proof end;

theorem :: TEX_1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for d0 being Element of D
for Y being non empty TopSpace holds
( TopStruct(# the carrier of Y,the topology of Y #) = TopStruct(# the carrier of (STS D,d0),the topology of (STS D,d0) #) iff ( the carrier of Y = D & ( for A being non empty Subset of Y holds Cl A = A \/ {d0} ) ) )
proof end;

theorem :: TEX_1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for d0 being Element of D
for Y being non empty TopSpace holds
( TopStruct(# the carrier of Y,the topology of Y #) = TopStruct(# the carrier of (STS D,d0),the topology of (STS D,d0) #) iff ( the carrier of Y = D & ( for A being Subset of Y st A <> D holds
Int A = A \ {d0} ) ) )
proof end;

Lm2: now
let D be non empty set ; :: thesis: for d0 being Element of D
for G being set st G = { P where P is Subset of D : ( d0 in P & P <> D ) } & D = {d0} holds
not G <> {}

let d0 be Element of D; :: thesis: for G being set st G = { P where P is Subset of D : ( d0 in P & P <> D ) } & D = {d0} holds
not G <> {}

let G be set ; :: thesis: ( G = { P where P is Subset of D : ( d0 in P & P <> D ) } & D = {d0} implies not G <> {} )
assume A1: G = { P where P is Subset of D : ( d0 in P & P <> D ) } ; :: thesis: ( D = {d0} implies not G <> {} )
assume A2: D = {d0} ; :: thesis: not G <> {}
assume A3: G <> {} ; :: thesis: contradiction
consider x being Element of G;
x in G by A3;
then consider S being Subset of D such that
x = S and
A4: d0 in S and
A5: S <> D by A1;
A6: now
assume D \ S = {} ; :: thesis: contradiction
then D c= S by XBOOLE_1:37;
hence contradiction by A5, XBOOLE_0:def 10; :: thesis: verum
end;
consider d1 being Element of D \ S;
reconsider d1 = d1 as Element of D by A6, XBOOLE_0:def 4;
d0 <> d1 by A4, A6, XBOOLE_0:def 4;
hence contradiction by A2, TARSKI:def 1; :: thesis: verum
end;

theorem :: TEX_1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for d0 being Element of D holds
( STS D,d0 = ADTS D iff D = {d0} )
proof end;

theorem :: TEX_1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for d0 being Element of D holds
( STS D,d0 = 1TopSp D iff D = {d0} )
proof end;

theorem :: TEX_1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for d0 being Element of D
for A being Subset of (STS D,d0) st A = {d0} holds
1TopSp D = (STS D,d0) modified_with_respect_to A
proof end;

definition
let X be non empty TopSpace;
redefine attr X is discrete means :Def6: :: TEX_1:def 6
for A being non empty Subset of X holds not A is boundary;
compatibility
( X is discrete iff for A being non empty Subset of X holds not A is boundary )
proof end;
end;

:: deftheorem Def6 defines discrete TEX_1:def 6 :
for X being non empty TopSpace holds
( X is discrete iff for A being non empty Subset of X holds not A is boundary );

theorem :: TEX_1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty TopSpace holds
( X is discrete iff for A being Subset of X st A <> the carrier of X holds
not A is dense )
proof end;

registration
cluster non empty non almost_discrete -> non empty non trivial non discrete non anti-discrete TopStruct ;
coherence
for b1 being non empty TopSpace st not b1 is almost_discrete holds
( not b1 is discrete & not b1 is anti-discrete )
proof end;
end;

definition
let X be non empty TopSpace;
redefine attr X is almost_discrete means :Def7: :: TEX_1:def 7
for A being non empty Subset of X holds not A is nowhere_dense;
compatibility
( X is almost_discrete iff for A being non empty Subset of X holds not A is nowhere_dense )
proof end;
end;

:: deftheorem Def7 defines almost_discrete TEX_1:def 7 :
for X being non empty TopSpace holds
( X is almost_discrete iff for A being non empty Subset of X holds not A is nowhere_dense );

theorem Th36: :: TEX_1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty TopSpace holds
( X is almost_discrete iff for A being Subset of X st A <> the carrier of X holds
not A is everywhere_dense )
proof end;

theorem Th37: :: TEX_1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty TopSpace holds
( not X is almost_discrete iff ex A being non empty Subset of X st
( A is boundary & A is closed ) )
proof end;

theorem :: TEX_1:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty TopSpace holds
( not X is almost_discrete iff ex A being Subset of X st
( A <> the carrier of X & A is dense & A is open ) )
proof end;

registration
cluster non empty non trivial strict non discrete non anti-discrete almost_discrete TopStruct ;
existence
ex b1 being TopSpace st
( b1 is almost_discrete & not b1 is discrete & not b1 is anti-discrete & b1 is strict & not b1 is empty )
proof end;
end;

theorem Th39: :: TEX_1:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for c0 being Element of C holds
( not C \ {c0} is empty iff not STS C,c0 is almost_discrete )
proof end;

registration
cluster non empty non trivial strict non discrete non anti-discrete non almost_discrete TopStruct ;
existence
ex b1 being TopSpace st
( not b1 is almost_discrete & b1 is strict & not b1 is empty )
proof end;
end;

theorem :: TEX_1:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty TopSpace
for A being non empty Subset of X st A is boundary holds
not X modified_with_respect_to (A ` ) is almost_discrete
proof end;

theorem :: TEX_1:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty TopSpace
for A being Subset of X st A <> the carrier of X & A is dense holds
not X modified_with_respect_to A is almost_discrete
proof end;