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

registration
let S be finite 1-sorted ;
cluster the carrier of S -> finite ;
coherence
the carrier of S is finite by GROUP_1:def 14;
end;

registration
let S be trivial 1-sorted ;
cluster the carrier of S -> trivial ;
coherence
the carrier of S is trivial by REALSET2:def 5;
end;

registration
cluster trivial -> finite set ;
coherence
for b1 being set st b1 is trivial holds
b1 is finite
proof end;
end;

registration
cluster trivial -> finite 1-sorted ;
coherence
for b1 being 1-sorted st b1 is trivial holds
b1 is finite
proof end;
end;

registration
cluster non trivial -> non empty 1-sorted ;
coherence
for b1 being 1-sorted st not b1 is trivial holds
not b1 is empty
proof end;
end;

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

theorem Th1: :: YELLOW13:1  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 being_T1 TopSpace
for A being finite Subset of T holds A is closed
proof end;

registration
let T be non empty being_T1 TopSpace;
cluster finite -> closed Element of bool the carrier of T;
coherence
for b1 being Subset of T st b1 is finite holds
b1 is closed by Th1;
end;

registration
let T be compact TopStruct ;
cluster [#] T -> compact ;
coherence
[#] T is compact by COMPTS_1:10;
end;

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

registration
cluster non empty being_T1 finite -> non empty discrete TopStruct ;
coherence
for b1 being non empty TopSpace st b1 is finite & b1 is being_T1 holds
b1 is discrete
proof end;
end;

registration
cluster finite -> compact TopStruct ;
coherence
for b1 being TopSpace st b1 is finite holds
b1 is compact
proof end;
end;

theorem Th2: :: YELLOW13:2  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 discrete TopSpace holds T is_T4
proof end;

theorem Th3: :: YELLOW13:3  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 discrete TopSpace holds T is_T3
proof end;

theorem Th4: :: YELLOW13:4  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 discrete TopSpace holds T is_T2
proof end;

theorem Th5: :: YELLOW13:5  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 discrete TopSpace holds T is_T1
proof end;

registration
cluster non empty discrete -> being_T1 being_T2 being_T3 being_T4 TopStruct ;
coherence
for b1 being TopSpace st b1 is discrete & not b1 is empty holds
( b1 is being_T4 & b1 is being_T3 & b1 is being_T2 & b1 is being_T1 ) by Th2, Th3, Th4, Th5;
end;

registration
cluster non empty being_T1 being_T4 -> non empty being_T3 TopStruct ;
coherence
for b1 being non empty TopSpace st b1 is being_T4 & b1 is being_T1 holds
b1 is being_T3
proof end;
end;

registration
cluster being_T1 being_T3 -> being_T2 TopStruct ;
coherence
for b1 being TopSpace st b1 is being_T3 & b1 is being_T1 holds
b1 is being_T2
proof end;
end;

registration
cluster being_T2 -> being_T1 TopStruct ;
coherence
for b1 being TopSpace st b1 is being_T2 holds
b1 is being_T1
proof end;
end;

registration
cluster being_T1 -> T_0 TopStruct ;
coherence
for b1 being TopSpace st b1 is being_T1 holds
b1 is T_0
proof end;
end;

theorem Th6: :: YELLOW13:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being reflexive RelStr
for T being reflexive transitive RelStr
for f being Function of S,T
for X being Subset of S holds downarrow (f .: X) c= downarrow (f .: (downarrow X))
proof end;

theorem :: YELLOW13:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being reflexive RelStr
for T being reflexive transitive RelStr
for f being Function of S,T
for X being Subset of S st f is monotone holds
downarrow (f .: X) = downarrow (f .: (downarrow X))
proof end;

theorem Th8: :: YELLOW13:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being non empty Poset holds IdsMap N is one-to-one
proof end;

registration
let N be non empty Poset;
cluster IdsMap N -> V6 ;
coherence
IdsMap N is one-to-one by Th8;
end;

theorem Th9: :: YELLOW13:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being finite LATTICE holds SupMap N is one-to-one
proof end;

registration
let N be finite LATTICE;
cluster SupMap N -> V6 ;
coherence
SupMap N is one-to-one by Th9;
end;

theorem :: YELLOW13:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being finite LATTICE holds N, InclPoset (Ids N) are_isomorphic
proof end;

theorem Th11: :: YELLOW13:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being non empty complete Poset
for x being Element of N
for X being non empty Subset of N holds x "/\" preserves_inf_of X
proof end;

theorem Th12: :: YELLOW13:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being non empty complete Poset
for x being Element of N holds x "/\" is meet-preserving
proof end;

registration
let N be non empty complete Poset;
let x be Element of N;
cluster x "/\" -> meet-preserving ;
coherence
x "/\" is meet-preserving by Th12;
end;

theorem :: YELLOW13:13  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 anti-discrete TopStruct
for p being Point of T holds {the carrier of T} is Basis of p
proof end;

theorem :: YELLOW13:14  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 anti-discrete TopStruct
for p being Point of T
for D being Basis of p holds D = {the carrier of T}
proof end;

theorem :: YELLOW13:15  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 Basis of T
for p being Point of T holds { A where A is Subset of T : ( A in P & p in A ) } is Basis of p
proof end;

Lm1: for T being non empty TopStruct
for A being Subset of T
for p being Point of T st p in Cl A holds
for K being Basis of p
for Q being Subset of T st Q in K holds
A meets Q
proof end;

Lm2: for T being non empty TopStruct
for A being Subset of T
for p being Point of T st ( for K being Basis of p
for Q being Subset of T st Q in K holds
A meets Q ) holds
ex K being Basis of p st
for Q being Subset of T st Q in K holds
A meets Q
proof end;

Lm3: for T being non empty TopStruct
for A being Subset of T
for p being Point of T st ex K being Basis of p st
for Q being Subset of T st Q in K holds
A meets Q holds
p in Cl A
proof end;

theorem :: YELLOW13:16  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 A being Subset of T
for p being Point of T holds
( p in Cl A iff for K being Basis of p
for Q being Subset of T st Q in K holds
A meets Q )
proof end;

theorem :: YELLOW13: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 TopStruct
for A being Subset of T
for p being Point of T holds
( p in Cl A iff ex K being Basis of p st
for Q being Subset of T st Q in K holds
A meets Q )
proof end;

definition
let T be TopStruct ;
let p be Point of T;
mode basis of p -> Subset-Family of T means :Def1: :: YELLOW13:def 1
for A being Subset of T st p in Int A holds
ex P being Subset of T st
( P in it & p in Int P & P c= A );
existence
ex b1 being Subset-Family of T st
for A being Subset of T st p in Int A holds
ex P being Subset of T st
( P in b1 & p in Int P & P c= A )
proof end;
end;

:: deftheorem Def1 defines basis YELLOW13:def 1 :
for T being TopStruct
for p being Point of T
for b3 being Subset-Family of T holds
( b3 is basis of p iff for A being Subset of T st p in Int A holds
ex P being Subset of T st
( P in b3 & p in Int P & P c= A ) );

definition
let T be non empty TopSpace;
let p be Point of T;
redefine mode basis of p means :: YELLOW13:def 2
for A being a_neighborhood of p ex P being a_neighborhood of p st
( P in it & P c= A );
compatibility
for b1 being Subset-Family of T holds
( b1 is basis of p iff for A being a_neighborhood of p ex P being a_neighborhood of p st
( P in b1 & P c= A ) )
proof end;
end;

:: deftheorem defines basis YELLOW13:def 2 :
for T being non empty TopSpace
for p being Point of T
for b3 being Subset-Family of T holds
( b3 is basis of p iff for A being a_neighborhood of p ex P being a_neighborhood of p st
( P in b3 & P c= A ) );

theorem Th18: :: YELLOW13: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 p being Point of T holds bool the carrier of T is basis of p
proof end;

theorem Th19: :: YELLOW13:19  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
for P being basis of p holds not P is empty
proof end;

registration
let T be non empty TopSpace;
let p be Point of T;
cluster -> non empty basis of p;
coherence
for b1 being basis of p holds not b1 is empty by Th19;
end;

registration
let T be TopStruct ;
let p be Point of T;
cluster non empty basis of p;
existence
not for b1 being basis of p holds b1 is empty
proof end;
end;

definition
let T be TopStruct ;
let p be Point of T;
let P be basis of p;
attr P is correct means :Def3: :: YELLOW13:def 3
for A being Subset of T holds
( A in P iff p in Int A );
end;

:: deftheorem Def3 defines correct YELLOW13:def 3 :
for T being TopStruct
for p being Point of T
for P being basis of p holds
( P is correct iff for A being Subset of T holds
( A in P iff p in Int A ) );

Lm4: now
let T be TopStruct ; :: thesis: for p being Point of T
for K being set st K = { A where A is Subset of T : p in Int A } holds
K is basis of p
let p be Point of T; :: thesis: for K being set st K = { A where A is Subset of T : p in Int A } holds
K is basis of p
let K be set ; :: thesis: ( K = { A where A is Subset of T : p in Int A } implies K is basis of p )
assume A1: K = { A where A is Subset of T : p in Int A } ; :: thesis: K is basis of p
K c= bool the carrier of T
proof
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in K or y in bool the carrier of T )
assume y in K ; :: thesis: y in bool the carrier of T
then consider A being Subset of T such that
A2: y = A and
p in Int A by A1;
thus y in bool the carrier of T by A2; :: thesis: verum
end;
then reconsider J = K as Subset-Family of T ;
reconsider J = J as Subset-Family of T ;
for A being Subset of T st p in Int A holds
ex P being Subset of T st
( P in J & p in Int P & P c= A )
proof
let A be Subset of T; :: thesis: ( p in Int A implies ex P being Subset of T st
( P in J & p in Int P & P c= A ) )
assume A3: p in Int A ; :: thesis: ex P being Subset of T st
( P in J & p in Int P & P c= A )
take P = A; :: thesis: ( P in J & p in Int P & P c= A )
thus ( P in J & p in Int P & P c= A ) by A1, A3; :: thesis: verum
end;
hence K is basis of p by Def1; :: thesis: verum
end;

Lm5: now
let T be TopStruct ; :: thesis: for p being Point of T
for K being basis of p st K = { A where A is Subset of T : p in Int A } holds
K is correct
let p be Point of T; :: thesis: for K being basis of p st K = { A where A is Subset of T : p in Int A } holds
K is correct
let K be basis of p; :: thesis: ( K = { A where A is Subset of T : p in Int A } implies K is correct )
assume A1: K = { A where A is Subset of T : p in Int A } ; :: thesis: K is correct
thus K is correct :: thesis: verum
proof
let A be Subset of T; :: according to YELLOW13:def 3 :: thesis: ( A in K iff p in Int A )
hereby :: thesis: ( p in Int A implies A in K )
assume A in K ; :: thesis: p in Int A
then consider M being Subset of T such that
A2: ( A = M & p in Int M ) by A1;
thus p in Int A by A2; :: thesis: verum
end;
thus ( p in Int A implies A in K ) by A1; :: thesis: verum
end;
end;

registration
let T be TopStruct ;
let p be Point of T;
cluster correct basis of p;
existence
ex b1 being basis of p st b1 is correct
proof end;
end;

theorem :: YELLOW13:20  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 p being Point of T holds { A where A is Subset of T : p in Int A } is correct basis of p by Lm4, Lm5;

registration
let T be non empty TopSpace;
let p be Point of T;
cluster non empty correct basis of p;
existence
ex b1 being basis of p st
( not b1 is empty & b1 is correct )
proof end;
end;

theorem :: YELLOW13: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 anti-discrete TopStruct
for p being Point of T holds {the carrier of T} is correct basis of p
proof end;

theorem :: YELLOW13: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 anti-discrete TopStruct
for p being Point of T
for D being correct basis of p holds D = {the carrier of T}
proof end;

theorem :: YELLOW13: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 TopSpace
for p being Point of T
for P being Basis of p holds P is basis of p
proof end;

definition
let T be TopStruct ;
mode basis of T -> Subset-Family of T means :Def4: :: YELLOW13:def 4
for p being Point of T holds it is basis of p;
existence
ex b1 being Subset-Family of T st
for p being Point of T holds b1 is basis of p
proof end;
end;

:: deftheorem Def4 defines basis YELLOW13:def 4 :
for T being TopStruct
for b2 being Subset-Family of T holds
( b2 is basis of T iff for p being Point of T holds b2 is basis of p );

theorem Th24: :: YELLOW13:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being TopStruct holds bool the carrier of T is basis of T
proof end;

theorem Th25: :: YELLOW13: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 P being basis of T holds not P is empty
proof end;

registration
let T be non empty TopSpace;
cluster -> non empty basis of T;
coherence
for b1 being basis of T holds not b1 is empty by Th25;
end;

registration
let T be TopStruct ;
cluster non empty basis of T;
existence
not for b1 being basis of T holds b1 is empty
proof end;
end;

theorem :: YELLOW13: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 basis of T holds the topology of T c= UniCl (Int P)
proof end;

theorem :: YELLOW13:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being TopSpace
for P being Basis of T holds P is basis of T
proof end;

definition
let T be non empty TopSpace-like TopRelStr ;
attr T is topological_semilattice means :Def5: :: YELLOW13:def 5
for f being Function of [:T,T:],T st f = inf_op T holds
f is continuous;
end;

:: deftheorem Def5 defines topological_semilattice YELLOW13:def 5 :
for T being non empty TopSpace-like TopRelStr holds
( T is topological_semilattice iff for f being Function of [:T,T:],T st f = inf_op T holds
f is continuous );

registration
cluster non empty TopSpace-like reflexive trivial -> non empty TopSpace-like topological_semilattice TopRelStr ;
coherence
for b1 being non empty TopSpace-like TopRelStr st b1 is reflexive & b1 is trivial holds
b1 is topological_semilattice
proof end;
end;

registration
cluster non empty TopSpace-like T_0 being_T1 reflexive compact being_T2 being_T3 being_T4 finite trivial topological_semilattice TopRelStr ;
existence
ex b1 being TopRelStr st
( b1 is reflexive & b1 is trivial & not b1 is empty & b1 is TopSpace-like )
proof end;
end;

theorem Th28: :: YELLOW13: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-like topological_semilattice TopRelStr
for x being Element of T holds x "/\" is continuous
proof end;

registration
let T be non empty TopSpace-like topological_semilattice TopRelStr ;
let x be Element of T;
cluster x "/\" -> continuous ;
coherence
x "/\" is continuous by Th28;
end;