:: by Artur Korni{\l}owicz

::

:: Received November 3, 1998

:: Copyright (c) 1998-2016 Association of Mizar Users

registration

let T be non empty T_1 TopSpace;

coherence

for b_{1} being Subset of T st b_{1} is finite holds

b_{1} is closed
by Th1;

end;
coherence

for b

b

registration
end;

registration

coherence

for b_{1} being non empty TopSpace st b_{1} is finite & b_{1} is T_1 holds

b_{1} is discrete

end;
for b

b

proof end;

registration

coherence

for b_{1} being TopSpace st b_{1} is discrete & not b_{1} is empty holds

( b_{1} is normal & b_{1} is regular & b_{1} is T_2 & b_{1} is T_1 )
by Th2, Th3, Th4, Th5;

end;
for b

( b

registration
end;

theorem Th6: :: YELLOW13:6

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))

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

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))

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;

registration
end;

registration
end;

theorem Th11: :: YELLOW13:11

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

for x being Element of N

for X being non empty Subset of N holds x "/\" preserves_inf_of X

proof end;

registration

let N be non empty complete Poset;

let x be Element of N;

coherence

x "/\" is meet-preserving by Th12;

end;
let x be Element of N;

coherence

x "/\" is meet-preserving by Th12;

theorem :: YELLOW13:13

for T being non empty anti-discrete TopStruct

for p being Point of T holds { the carrier of T} is Basis of

for p being Point of T holds { the carrier of T} is Basis of

proof end;

theorem :: YELLOW13:14

for T being non empty anti-discrete TopStruct

for p being Point of T

for D being Basis of holds D = { the carrier of T}

for p being Point of T

for D being Basis of holds D = { the carrier of T}

proof end;

theorem :: YELLOW13:15

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

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

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

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

for Q being Subset of T st Q in K holds

A meets Q ) holds

ex K being Basis of 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 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

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

for Q being Subset of T st Q in K holds

A meets Q )

for A being Subset of T

for p being Point of T holds

( p in Cl A iff for K being Basis of

for Q being Subset of T st Q in K holds

A meets Q )

proof end;

theorem :: YELLOW13:17

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 st

for Q being Subset of T st Q in K holds

A meets Q )

for A being Subset of T

for p being Point of T holds

( p in Cl A iff ex K being Basis of 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;

ex b_{1} 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 b_{1} & p in Int P & P c= A )

end;
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 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 );

ex b

for A being Subset of T st p in Int A holds

ex P being Subset of T st

( P in b

proof end;

:: deftheorem Def1 defines basis YELLOW13:def 1 :

for T being TopStruct

for p being Point of T

for b_{3} being Subset-Family of T holds

( b_{3} 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 b_{3} & p in Int P & P c= A ) );

for T being TopStruct

for p being Point of T

for b

( b

ex P being Subset of T st

( P in b

definition

let T be non empty TopSpace;

let p be Point of T;

for b_{1} being Subset-Family of T holds

( b_{1} is basis of p iff for A being a_neighborhood of p ex P being a_neighborhood of p st

( P in b_{1} & P c= A ) )

end;
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 A being a_neighborhood of p ex P being a_neighborhood of p st

( P in it & P c= A );

for b

( b

( P in b

proof end;

:: deftheorem defines basis YELLOW13:def 2 :

for T being non empty TopSpace

for p being Point of T

for b_{3} being Subset-Family of T holds

( b_{3} is basis of p iff for A being a_neighborhood of p ex P being a_neighborhood of p st

( P in b_{3} & P c= A ) );

for T being non empty TopSpace

for p being Point of T

for b

( b

( P in b

registration

let T be non empty TopSpace;

let p be Point of T;

coherence

for b_{1} being basis of p holds not b_{1} is empty
by Th19;

end;
let p be Point of T;

coherence

for b

registration

let T be TopStruct ;

let p be Point of T;

existence

not for b_{1} being basis of p holds b_{1} is empty

end;
let p be Point of T;

existence

not for b

proof 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 ) );

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 :: thesis: for T being TopStruct

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

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 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

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 )

end;
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

then reconsider J = K as Subset-Family of T ;
let y be object ; :: 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 ex A being Subset of T st

( y = A & p in Int A ) by A1;

hence y in bool the carrier of T ; :: thesis: verum

end;
assume y in K ; :: thesis: y in bool the carrier of T

then ex A being Subset of T st

( y = A & p in Int A ) by A1;

hence y in bool the carrier of T ; :: thesis: verum

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

hence
K is basis of p
by Def1; :: thesis: verum
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 A2: 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, A2; :: thesis: verum

end;
( P in J & p in Int P & P c= A ) )

assume A2: 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, A2; :: thesis: verum

Lm5: now :: thesis: for T being TopStruct

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

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 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

end;
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 )

end;
hereby :: thesis: ( p in Int A implies A in K )

thus
( p in Int A implies A in K )
by A1; :: thesis: verum
assume
A in K
; :: thesis: p in Int A

then ex M being Subset of T st

( A = M & p in Int M ) by A1;

hence p in Int A ; :: thesis: verum

end;
then ex M being Subset of T st

( A = M & p in Int M ) by A1;

hence p in Int A ; :: thesis: verum

registration

let T be TopStruct ;

let p be Point of T;

existence

ex b_{1} being basis of p st b_{1} is correct

end;
let p be Point of T;

existence

ex b

proof end;

theorem :: YELLOW13:20

registration

let T be non empty TopSpace;

let p be Point of T;

existence

ex b_{1} being basis of p st

( not b_{1} is empty & b_{1} is correct )

end;
let p be Point of T;

existence

ex b

( not b

proof end;

theorem :: YELLOW13:21

for T being non empty anti-discrete TopStruct

for p being Point of T holds { the carrier of T} is correct basis of p

for p being Point of T holds { the carrier of T} is correct basis of p

proof end;

theorem :: YELLOW13:22

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}

for p being Point of T

for D being correct basis of p holds D = { the carrier of T}

proof end;

definition

let T be TopStruct ;

ex b_{1} being Subset-Family of T st

for p being Point of T holds b_{1} is basis of p

end;
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 for p being Point of T holds it is basis of p;

ex b

for p being Point of T holds b

proof end;

:: deftheorem Def4 defines basis YELLOW13:def 4 :

for T being TopStruct

for b_{2} being Subset-Family of T holds

( b_{2} is basis of T iff for p being Point of T holds b_{2} is basis of p );

for T being TopStruct

for b

( b

registration
end;

registration
end;

definition

let T be non empty TopSpace-like TopRelStr ;

end;
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 ;

for f being Function of [:T,T:],T st f = inf_op T holds

f is continuous ;

:: 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 );

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

for b_{1} being 1 -element TopSpace-like TopRelStr st b_{1} is reflexive holds

b_{1} is topological_semilattice
end;

cluster 1 -element TopSpace-like reflexive -> 1 -element TopSpace-like topological_semilattice for TopRelStr ;

coherence for b

b

proof end;

theorem Th28: :: YELLOW13:28

for T being non empty TopSpace-like topological_semilattice TopRelStr

for x being Element of T holds x "/\" is continuous

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;

coherence

x "/\" is continuous by Th28;

end;
let x be Element of T;

coherence

x "/\" is continuous by Th28;