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

theorem Th1: :: YELLOW_8:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, A, B being set st A in Fin X & B c= A holds
B in Fin X
proof end;

theorem Th2: :: YELLOW_8:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for F being Subset-Family of X st F c= Fin X holds
meet F in Fin X
proof end;

definition
let X be non empty set ;
redefine attr X is trivial means :Def1: :: YELLOW_8:def 1
for x, y being Element of X holds x = y;
compatibility
( X is trivial iff for x, y being Element of X holds x = y )
proof end;
end;

:: deftheorem Def1 defines trivial YELLOW_8:def 1 :
for X being non empty set holds
( X is trivial iff for x, y being Element of X holds x = y );

theorem :: YELLOW_8:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th4: :: YELLOW_8:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for F being Subset-Family of X holds F, COMPLEMENT F are_equipotent
proof end;

theorem Th5: :: YELLOW_8:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set st X,Y are_equipotent & X is countable holds
Y is countable
proof end;

theorem :: YELLOW_8:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: YELLOW_8:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: YELLOW_8:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: YELLOW_8:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: YELLOW_8:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: YELLOW_8:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: YELLOW_8:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: YELLOW_8:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: YELLOW_8:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being 1-sorted
for F being Subset-Family of X
for P being Subset of X holds
( P ` in COMPLEMENT F iff P in F )
proof end;

theorem Th15: :: YELLOW_8:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being 1-sorted
for F being Subset-Family of X holds Intersect (COMPLEMENT F) = (union F) `
proof end;

theorem Th16: :: YELLOW_8:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being 1-sorted
for F being Subset-Family of X holds union (COMPLEMENT F) = (Intersect F) `
proof end;

theorem :: YELLOW_8:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for A, B being Subset of T st B c= A & A is closed & ( for C being Subset of T st B c= C & C is closed holds
A c= C ) holds
A = Cl B
proof end;

theorem Th18: :: YELLOW_8:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being TopStruct
for B being Basis of T
for V being Subset of T st V is open holds
V = union { G where G is Subset of T : ( G in B & G c= V ) }
proof end;

theorem Th19: :: YELLOW_8:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being TopStruct
for B being Basis of T
for S being Subset of T st S in B holds
S is open
proof end;

theorem :: YELLOW_8:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for B being Basis of T
for V being Subset of T holds Int V = union { G where G is Subset of T : ( G in B & G c= V ) }
proof end;

definition
let T be non empty TopStruct ;
let x be Point of T;
mode Basis of x -> Subset-Family of T means :Def2: :: YELLOW_8:def 2
( it c= the topology of T & x in Intersect it & ( for S being Subset of T st S is open & x in S holds
ex V being Subset of T st
( V in it & V c= S ) ) );
existence
ex b1 being Subset-Family of T st
( b1 c= the topology of T & x in Intersect b1 & ( for S being Subset of T st S is open & x in S holds
ex V being Subset of T st
( V in b1 & V c= S ) ) )
proof end;
end;

:: deftheorem Def2 defines Basis YELLOW_8:def 2 :
for T being non empty TopStruct
for x being Point of T
for b3 being Subset-Family of T holds
( b3 is Basis of x iff ( b3 c= the topology of T & x in Intersect b3 & ( for S being Subset of T st S is open & x in S holds
ex V being Subset of T st
( V in b3 & V c= S ) ) ) );

theorem Th21: :: YELLOW_8:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopStruct
for x being Point of T
for B being Basis of x
for V being Subset of T st V in B holds
( V is open & x in V )
proof end;

theorem :: YELLOW_8:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopStruct
for x being Point of T
for B being Basis of x
for V being Subset of T st x in V & V is open holds
ex W being Subset of T st
( W in B & W c= V ) by Def2;

theorem :: YELLOW_8:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopStruct
for P being Subset-Family of T st P c= the topology of T & ( for x being Point of T ex B being Basis of x st B c= P ) holds
P is Basis of T
proof end;

definition
let T be non empty TopSpace;
attr T is Baire means :Def3: :: YELLOW_8:def 3
for F being Subset-Family of T st F is countable & ( for S being Subset of T st S in F holds
S is everywhere_dense ) holds
ex I being Subset of T st
( I = Intersect F & I is dense );
end;

:: deftheorem Def3 defines Baire YELLOW_8:def 3 :
for T being non empty TopSpace holds
( T is Baire iff for F being Subset-Family of T st F is countable & ( for S being Subset of T st S in F holds
S is everywhere_dense ) holds
ex I being Subset of T st
( I = Intersect F & I is dense ) );

theorem :: YELLOW_8:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace holds
( T is Baire iff for F being Subset-Family of T st F is countable & ( for S being Subset of T st S in F holds
S is nowhere_dense ) holds
union F is boundary )
proof end;

definition
let T be TopStruct ;
let S be Subset of T;
attr S is irreducible means :Def4: :: YELLOW_8:def 4
( not S is empty & S is closed & ( for S1, S2 being Subset of T st S1 is closed & S2 is closed & S = S1 \/ S2 & not S1 = S holds
S2 = S ) );
end;

:: deftheorem Def4 defines irreducible YELLOW_8:def 4 :
for T being TopStruct
for S being Subset of T holds
( S is irreducible iff ( not S is empty & S is closed & ( for S1, S2 being Subset of T st S1 is closed & S2 is closed & S = S1 \/ S2 & not S1 = S holds
S2 = S ) ) );

registration
let T be TopStruct ;
cluster irreducible -> non empty Element of bool the carrier of T;
coherence
for b1 being Subset of T st b1 is irreducible holds
not b1 is empty
by Def4;
end;

definition
let T be non empty TopSpace;
let S be Subset of T;
let p be Point of T;
pred p is_dense_point_of S means :Def5: :: YELLOW_8:def 5
( p in S & S c= Cl {p} );
end;

:: deftheorem Def5 defines is_dense_point_of YELLOW_8:def 5 :
for T being non empty TopSpace
for S being Subset of T
for p being Point of T holds
( p is_dense_point_of S iff ( p in S & S c= Cl {p} ) );

theorem :: YELLOW_8:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for S being Subset of T st S is closed holds
for p being Point of T st p is_dense_point_of S holds
S = Cl {p}
proof end;

theorem Th26: :: YELLOW_8:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for p being Point of T holds Cl {p} is irreducible
proof end;

registration
let T be non empty TopSpace;
cluster non empty irreducible Element of bool the carrier of T;
existence
ex b1 being Subset of T st b1 is irreducible
proof end;
end;

definition
let T be non empty TopSpace;
attr T is sober means :Def6: :: YELLOW_8:def 6
for S being irreducible Subset of T ex p being Point of T st
( p is_dense_point_of S & ( for q being Point of T st q is_dense_point_of S holds
p = q ) );
end;

:: deftheorem Def6 defines sober YELLOW_8:def 6 :
for T being non empty TopSpace holds
( T is sober iff for S being irreducible Subset of T ex p being Point of T st
( p is_dense_point_of S & ( for q being Point of T st q is_dense_point_of S holds
p = q ) ) );

theorem Th27: :: YELLOW_8:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for p being Point of T holds p is_dense_point_of Cl {p}
proof end;

theorem Th28: :: YELLOW_8:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for p being Point of T holds p is_dense_point_of {p}
proof end;

theorem Th29: :: YELLOW_8:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for G, F being Subset of T st G is open & F is closed holds
F \ G is closed
proof end;

theorem Th30: :: YELLOW_8:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty Hausdorff TopSpace
for S being irreducible Subset of T holds S is trivial
proof end;

registration
let T be non empty Hausdorff TopSpace;
cluster irreducible -> trivial Element of bool the carrier of T;
coherence
for b1 being Subset of T st b1 is irreducible holds
b1 is trivial
by Th30;
end;

theorem Th31: :: YELLOW_8:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty Hausdorff TopSpace holds T is sober
proof end;

registration
cluster non empty Hausdorff -> non empty sober TopStruct ;
coherence
for b1 being non empty TopSpace st b1 is being_T2 holds
b1 is sober
by Th31;
end;

registration
cluster non empty sober TopStruct ;
existence
ex b1 being non empty TopSpace st b1 is sober
proof end;
end;

theorem Th32: :: YELLOW_8:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace holds
( T is T_0 iff for p, q being Point of T st Cl {p} = Cl {q} holds
p = q )
proof end;

theorem Th33: :: YELLOW_8:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty sober TopSpace holds T is T_0
proof end;

registration
cluster non empty sober -> non empty T_0 TopStruct ;
coherence
for b1 being non empty TopSpace st b1 is sober holds
b1 is T_0
by Th33;
end;

definition
let X be set ;
func CofinTop X -> strict TopStruct means :Def7: :: YELLOW_8:def 7
( the carrier of it = X & COMPLEMENT the topology of it = {X} \/ (Fin X) );
existence
ex b1 being strict TopStruct st
( the carrier of b1 = X & COMPLEMENT the topology of b1 = {X} \/ (Fin X) )
proof end;
uniqueness
for b1, b2 being strict TopStruct st the carrier of b1 = X & COMPLEMENT the topology of b1 = {X} \/ (Fin X) & the carrier of b2 = X & COMPLEMENT the topology of b2 = {X} \/ (Fin X) holds
b1 = b2
by SETFAM_1:53;
end;

:: deftheorem Def7 defines CofinTop YELLOW_8:def 7 :
for X being set
for b2 being strict TopStruct holds
( b2 = CofinTop X iff ( the carrier of b2 = X & COMPLEMENT the topology of b2 = {X} \/ (Fin X) ) );

registration
let X be non empty set ;
cluster CofinTop X -> non empty strict ;
coherence
not CofinTop X is empty
proof end;
end;

registration
let X be set ;
cluster CofinTop X -> strict TopSpace-like ;
coherence
CofinTop X is TopSpace-like
proof end;
end;

theorem Th34: :: YELLOW_8:34  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 set
for P being Subset of (CofinTop X) holds
( P is closed iff ( P = X or P is finite ) )
proof end;

theorem Th35: :: YELLOW_8:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace st T is_T1 holds
for p being Point of T holds Cl {p} = {p}
proof end;

registration
let X be non empty set ;
cluster CofinTop X -> non empty strict TopSpace-like being_T1 ;
coherence
CofinTop X is being_T1
proof end;
end;

registration
let X be infinite set ;
cluster CofinTop X -> non empty strict TopSpace-like being_T1 non sober ;
coherence
not CofinTop X is sober
proof end;
end;

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

theorem Th36: :: YELLOW_8:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace holds
( T is_T3 iff for p being Point of T
for P being Subset of T st p in Int P holds
ex Q being Subset of T st
( Q is closed & Q c= P & p in Int Q ) )
proof end;

theorem :: YELLOW_8:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace st T is_T3 holds
( T is locally-compact iff for x being Point of T ex Y being Subset of T st
( x in Int Y & Y is compact ) )
proof end;