:: by Artur Korni{\l}owicz

::

:: Received December 20, 1996

:: Copyright (c) 1996-2019 Association of Mizar Users

registration
end;

definition

let S, T be non empty RelStr ;

let f be Function of S,T;

( f is antitone iff for x, y being Element of S st x <= y holds

f . x >= f . y ) ;

end;
let f be Function of S,T;

redefine attr f is antitone means :: WAYBEL_9:def 1

for x, y being Element of S st x <= y holds

f . x >= f . y;

compatibility for x, y being Element of S st x <= y holds

f . x >= f . y;

( f is antitone iff for x, y being Element of S st x <= y holds

f . x >= f . y ) ;

:: deftheorem defines antitone WAYBEL_9:def 1 :

for S, T being non empty RelStr

for f being Function of S,T holds

( f is antitone iff for x, y being Element of S st x <= y holds

f . x >= f . y );

for S, T being non empty RelStr

for f being Function of S,T holds

( f is antitone iff for x, y being Element of S st x <= y holds

f . x >= f . y );

theorem Th1: :: WAYBEL_9:1

for S, T being RelStr

for K, L being non empty RelStr

for f being Function of S,T

for g being Function of K,L st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of K, the InternalRel of K #) & RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of L, the InternalRel of L #) & f = g & f is monotone holds

g is monotone

for K, L being non empty RelStr

for f being Function of S,T

for g being Function of K,L st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of K, the InternalRel of K #) & RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of L, the InternalRel of L #) & f = g & f is monotone holds

g is monotone

proof end;

theorem Th2: :: WAYBEL_9:2

for S, T being RelStr

for K, L being non empty RelStr

for f being Function of S,T

for g being Function of K,L st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of K, the InternalRel of K #) & RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of L, the InternalRel of L #) & f = g & f is antitone holds

g is antitone

for K, L being non empty RelStr

for f being Function of S,T

for g being Function of K,L st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of K, the InternalRel of K #) & RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of L, the InternalRel of L #) & f = g & f is antitone holds

g is antitone

proof end;

theorem :: WAYBEL_9:3

for A, B being 1-sorted

for F being Subset-Family of A

for G being Subset-Family of B st the carrier of A = the carrier of B & F = G & F is Cover of A holds

G is Cover of B ;

for F being Subset-Family of A

for G being Subset-Family of B st the carrier of A = the carrier of B & F = G & F is Cover of A holds

G is Cover of B ;

Lm1: for L being reflexive antisymmetric with_infima RelStr

for x being Element of L holds uparrow x = { z where z is Element of L : z "/\" x = x }

proof end;

theorem Th4: :: WAYBEL_9:4

for L being reflexive antisymmetric with_suprema RelStr

for x being Element of L holds uparrow x = {x} "\/" ([#] L)

for x being Element of L holds uparrow x = {x} "\/" ([#] L)

proof end;

Lm2: for L being reflexive antisymmetric with_suprema RelStr

for x being Element of L holds downarrow x = { z where z is Element of L : z "\/" x = x }

proof end;

theorem Th5: :: WAYBEL_9:5

for L being reflexive antisymmetric with_infima RelStr

for x being Element of L holds downarrow x = {x} "/\" ([#] L)

for x being Element of L holds downarrow x = {x} "/\" ([#] L)

proof end;

theorem :: WAYBEL_9:6

for L being reflexive antisymmetric with_infima RelStr

for y being Element of L holds (y "/\") .: (uparrow y) = {y}

for y being Element of L holds (y "/\") .: (uparrow y) = {y}

proof end;

theorem Th7: :: WAYBEL_9:7

for L being reflexive antisymmetric with_infima RelStr

for x being Element of L holds (x "/\") " {x} = uparrow x

for x being Element of L holds (x "/\") " {x} = uparrow x

proof end;

theorem Th8: :: WAYBEL_9:8

for T being non empty 1-sorted

for N being non empty NetStr over T holds N is_eventually_in rng the mapping of N

for N being non empty NetStr over T holds N is_eventually_in rng the mapping of N

proof end;

Lm3: for L being non empty reflexive transitive RelStr

for D being non empty directed Subset of L

for n being Function of D, the carrier of L holds NetStr(# D,( the InternalRel of L |_2 D),n #) is net of L

proof end;

registration

let L be non empty reflexive RelStr ;

let D be non empty directed Subset of L;

let n be Function of D, the carrier of L;

coherence

NetStr(# D,( the InternalRel of L |_2 D),n #) is directed by WAYBEL_2:19;

end;
let D be non empty directed Subset of L;

let n be Function of D, the carrier of L;

coherence

NetStr(# D,( the InternalRel of L |_2 D),n #) is directed by WAYBEL_2:19;

registration

let L be non empty reflexive transitive RelStr ;

let D be non empty directed Subset of L;

let n be Function of D, the carrier of L;

coherence

NetStr(# D,( the InternalRel of L |_2 D),n #) is transitive by Lm3;

end;
let D be non empty directed Subset of L;

let n be Function of D, the carrier of L;

coherence

NetStr(# D,( the InternalRel of L |_2 D),n #) is transitive by Lm3;

:: cf WAYBEL_2:42

theorem Th9: :: WAYBEL_9:9

for L being non empty reflexive transitive RelStr st ( for x being Element of L

for N being net of L st N is eventually-directed holds

x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) ) holds

L is satisfying_MC

for N being net of L st N is eventually-directed holds

x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) ) holds

L is satisfying_MC

proof end;

theorem Th10: :: WAYBEL_9:10

for L being non empty RelStr

for a being Element of L

for N being net of L holds a "/\" N is net of L

for a being Element of L

for N being net of L holds a "/\" N is net of L

proof end;

registration

let L be non empty RelStr ;

let x be Element of L;

let N be net of L;

coherence

x "/\" N is transitive by Th10;

end;
let x be Element of L;

let N be net of L;

coherence

x "/\" N is transitive by Th10;

registration

let L be non empty RelStr ;

let x be Element of L;

let N be non empty reflexive NetStr over L;

coherence

x "/\" N is reflexive

end;
let x be Element of L;

let N be non empty reflexive NetStr over L;

coherence

x "/\" N is reflexive

proof end;

registration

let L be non empty RelStr ;

let x be Element of L;

let N be non empty antisymmetric NetStr over L;

coherence

x "/\" N is antisymmetric

end;
let x be Element of L;

let N be non empty antisymmetric NetStr over L;

coherence

x "/\" N is antisymmetric

proof end;

registration

let L be non empty RelStr ;

let x be Element of L;

let N be non empty transitive NetStr over L;

coherence

x "/\" N is transitive

end;
let x be Element of L;

let N be non empty transitive NetStr over L;

coherence

x "/\" N is transitive

proof end;

registration

let L be non empty RelStr ;

let J be set ;

let f be Function of J, the carrier of L;

coherence

FinSups f is transitive

end;
let J be set ;

let f be Function of J, the carrier of L;

coherence

FinSups f is transitive

proof end;

:: deftheorem defines inf WAYBEL_9:def 2 :

for L being non empty RelStr

for N being NetStr over L holds inf N = Inf ;

for L being non empty RelStr

for N being NetStr over L holds inf N = Inf ;

:: deftheorem defines ex_sup_of WAYBEL_9:def 3 :

for L being RelStr

for N being NetStr over L holds

( ex_sup_of N iff ex_sup_of rng the mapping of N,L );

for L being RelStr

for N being NetStr over L holds

( ex_sup_of N iff ex_sup_of rng the mapping of N,L );

:: deftheorem defines ex_inf_of WAYBEL_9:def 4 :

for L being RelStr

for N being NetStr over L holds

( ex_inf_of N iff ex_inf_of rng the mapping of N,L );

for L being RelStr

for N being NetStr over L holds

( ex_inf_of N iff ex_inf_of rng the mapping of N,L );

definition

let L be RelStr ;

ex b_{1} being strict NetStr over L st

( RelStr(# the carrier of b_{1}, the InternalRel of b_{1} #) = RelStr(# the carrier of L, the InternalRel of L #) & the mapping of b_{1} = id L )

for b_{1}, b_{2} being strict NetStr over L st RelStr(# the carrier of b_{1}, the InternalRel of b_{1} #) = RelStr(# the carrier of L, the InternalRel of L #) & the mapping of b_{1} = id L & RelStr(# the carrier of b_{2}, the InternalRel of b_{2} #) = RelStr(# the carrier of L, the InternalRel of L #) & the mapping of b_{2} = id L holds

b_{1} = b_{2}
;

end;
func L +id -> strict NetStr over L means :Def5: :: WAYBEL_9:def 5

( RelStr(# the carrier of it, the InternalRel of it #) = RelStr(# the carrier of L, the InternalRel of L #) & the mapping of it = id L );

existence ( RelStr(# the carrier of it, the InternalRel of it #) = RelStr(# the carrier of L, the InternalRel of L #) & the mapping of it = id L );

ex b

( RelStr(# the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def5 defines +id WAYBEL_9:def 5 :

for L being RelStr

for b_{2} being strict NetStr over L holds

( b_{2} = L +id iff ( RelStr(# the carrier of b_{2}, the InternalRel of b_{2} #) = RelStr(# the carrier of L, the InternalRel of L #) & the mapping of b_{2} = id L ) );

for L being RelStr

for b

( b

registration

let L be non empty RelStr ;

coherence

( L +id is monotone & L +id is eventually-directed )

end;
coherence

( L +id is monotone & L +id is eventually-directed )

proof end;

definition

let L be RelStr ;

ex b_{1} being strict NetStr over L st

( the carrier of b_{1} = the carrier of L & the InternalRel of b_{1} = the InternalRel of L ~ & the mapping of b_{1} = id L )

for b_{1}, b_{2} being strict NetStr over L st the carrier of b_{1} = the carrier of L & the InternalRel of b_{1} = the InternalRel of L ~ & the mapping of b_{1} = id L & the carrier of b_{2} = the carrier of L & the InternalRel of b_{2} = the InternalRel of L ~ & the mapping of b_{2} = id L holds

b_{1} = b_{2}
;

end;
func L opp+id -> strict NetStr over L means :Def6: :: WAYBEL_9:def 6

( the carrier of it = the carrier of L & the InternalRel of it = the InternalRel of L ~ & the mapping of it = id L );

existence ( the carrier of it = the carrier of L & the InternalRel of it = the InternalRel of L ~ & the mapping of it = id L );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def6 defines opp+id WAYBEL_9:def 6 :

for L being RelStr

for b_{2} being strict NetStr over L holds

( b_{2} = L opp+id iff ( the carrier of b_{2} = the carrier of L & the InternalRel of b_{2} = the InternalRel of L ~ & the mapping of b_{2} = id L ) );

for L being RelStr

for b

( b

theorem Th11: :: WAYBEL_9:11

for L being RelStr holds RelStr(# the carrier of (L ~), the InternalRel of (L ~) #) = RelStr(# the carrier of (L opp+id), the InternalRel of (L opp+id) #)

proof end;

registration

let L be non empty RelStr ;

coherence

( L opp+id is antitone & L opp+id is eventually-filtered )

end;
coherence

( L opp+id is antitone & L opp+id is eventually-filtered )

proof end;

definition

let L be non empty 1-sorted ;

let N be non empty NetStr over L;

let i be Element of N;

ex b_{1} being strict NetStr over L st

( ( for x being object holds

( x in the carrier of b_{1} iff ex y being Element of N st

( y = x & i <= y ) ) ) & the InternalRel of b_{1} = the InternalRel of N |_2 the carrier of b_{1} & the mapping of b_{1} = the mapping of N | the carrier of b_{1} )

for b_{1}, b_{2} being strict NetStr over L st ( for x being object holds

( x in the carrier of b_{1} iff ex y being Element of N st

( y = x & i <= y ) ) ) & the InternalRel of b_{1} = the InternalRel of N |_2 the carrier of b_{1} & the mapping of b_{1} = the mapping of N | the carrier of b_{1} & ( for x being object holds

( x in the carrier of b_{2} iff ex y being Element of N st

( y = x & i <= y ) ) ) & the InternalRel of b_{2} = the InternalRel of N |_2 the carrier of b_{2} & the mapping of b_{2} = the mapping of N | the carrier of b_{2} holds

b_{1} = b_{2}

end;
let N be non empty NetStr over L;

let i be Element of N;

func N | i -> strict NetStr over L means :Def7: :: WAYBEL_9:def 7

( ( for x being object holds

( x in the carrier of it iff ex y being Element of N st

( y = x & i <= y ) ) ) & the InternalRel of it = the InternalRel of N |_2 the carrier of it & the mapping of it = the mapping of N | the carrier of it );

existence ( ( for x being object holds

( x in the carrier of it iff ex y being Element of N st

( y = x & i <= y ) ) ) & the InternalRel of it = the InternalRel of N |_2 the carrier of it & the mapping of it = the mapping of N | the carrier of it );

ex b

( ( for x being object holds

( x in the carrier of b

( y = x & i <= y ) ) ) & the InternalRel of b

proof end;

uniqueness for b

( x in the carrier of b

( y = x & i <= y ) ) ) & the InternalRel of b

( x in the carrier of b

( y = x & i <= y ) ) ) & the InternalRel of b

b

proof end;

:: deftheorem Def7 defines | WAYBEL_9:def 7 :

for L being non empty 1-sorted

for N being non empty NetStr over L

for i being Element of N

for b_{4} being strict NetStr over L holds

( b_{4} = N | i iff ( ( for x being object holds

( x in the carrier of b_{4} iff ex y being Element of N st

( y = x & i <= y ) ) ) & the InternalRel of b_{4} = the InternalRel of N |_2 the carrier of b_{4} & the mapping of b_{4} = the mapping of N | the carrier of b_{4} ) );

for L being non empty 1-sorted

for N being non empty NetStr over L

for i being Element of N

for b

( b

( x in the carrier of b

( y = x & i <= y ) ) ) & the InternalRel of b

theorem :: WAYBEL_9:12

for L being non empty 1-sorted

for N being non empty NetStr over L

for i being Element of N holds the carrier of (N | i) = { y where y is Element of N : i <= y }

for N being non empty NetStr over L

for i being Element of N holds the carrier of (N | i) = { y where y is Element of N : i <= y }

proof end;

theorem Th13: :: WAYBEL_9:13

for L being non empty 1-sorted

for N being non empty NetStr over L

for i being Element of N holds the carrier of (N | i) c= the carrier of N

for N being non empty NetStr over L

for i being Element of N holds the carrier of (N | i) c= the carrier of N

proof end;

theorem Th14: :: WAYBEL_9:14

for L being non empty 1-sorted

for N being non empty NetStr over L

for i being Element of N holds N | i is full SubNetStr of N

for N being non empty NetStr over L

for i being Element of N holds N | i is full SubNetStr of N

proof end;

registration

let L be non empty 1-sorted ;

let N be non empty reflexive NetStr over L;

let i be Element of N;

coherence

( not N | i is empty & N | i is reflexive )

end;
let N be non empty reflexive NetStr over L;

let i be Element of N;

coherence

( not N | i is empty & N | i is reflexive )

proof end;

registration

let L be non empty 1-sorted ;

let N be non empty directed NetStr over L;

let i be Element of N;

coherence

not N | i is empty

end;
let N be non empty directed NetStr over L;

let i be Element of N;

coherence

not N | i is empty

proof end;

registration

let L be non empty 1-sorted ;

let N be non empty reflexive antisymmetric NetStr over L;

let i be Element of N;

coherence

N | i is antisymmetric

end;
let N be non empty reflexive antisymmetric NetStr over L;

let i be Element of N;

coherence

N | i is antisymmetric

proof end;

registration

let L be non empty 1-sorted ;

let N be non empty antisymmetric directed NetStr over L;

let i be Element of N;

coherence

N | i is antisymmetric

end;
let N be non empty antisymmetric directed NetStr over L;

let i be Element of N;

coherence

N | i is antisymmetric

proof end;

registration

let L be non empty 1-sorted ;

let N be non empty reflexive transitive NetStr over L;

let i be Element of N;

coherence

N | i is transitive

end;
let N be non empty reflexive transitive NetStr over L;

let i be Element of N;

coherence

N | i is transitive

proof end;

registration

let L be non empty 1-sorted ;

let N be net of L;

let i be Element of N;

coherence

( N | i is transitive & N | i is directed )

end;
let N be net of L;

let i be Element of N;

coherence

( N | i is transitive & N | i is directed )

proof end;

theorem :: WAYBEL_9:15

for L being non empty 1-sorted

for N being non empty reflexive NetStr over L

for i, x being Element of N

for x1 being Element of (N | i) st x = x1 holds

N . x = (N | i) . x1

for N being non empty reflexive NetStr over L

for i, x being Element of N

for x1 being Element of (N | i) st x = x1 holds

N . x = (N | i) . x1

proof end;

theorem Th16: :: WAYBEL_9:16

for L being non empty 1-sorted

for N being non empty directed NetStr over L

for i, x being Element of N

for x1 being Element of (N | i) st x = x1 holds

N . x = (N | i) . x1

for N being non empty directed NetStr over L

for i, x being Element of N

for x1 being Element of (N | i) st x = x1 holds

N . x = (N | i) . x1

proof end;

theorem Th17: :: WAYBEL_9:17

for L being non empty 1-sorted

for N being net of L

for i being Element of N holds N | i is subnet of N

for N being net of L

for i being Element of N holds N | i is subnet of N

proof end;

registration

let T be non empty 1-sorted ;

let N be net of T;

existence

ex b_{1} being subnet of N st b_{1} is strict

end;
let N be net of T;

existence

ex b

proof end;

definition

let L be non empty 1-sorted ;

let N be net of L;

let i be Element of N;

:: original: |

redefine func N | i -> strict subnet of N;

coherence

N | i is strict subnet of N by Th17;

end;
let N be net of L;

let i be Element of N;

:: original: |

redefine func N | i -> strict subnet of N;

coherence

N | i is strict subnet of N by Th17;

definition

let S be non empty 1-sorted ;

let T be 1-sorted ;

let f be Function of S,T;

let N be NetStr over S;

ex b_{1} being strict NetStr over T st

( RelStr(# the carrier of b_{1}, the InternalRel of b_{1} #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of b_{1} = f * the mapping of N )

for b_{1}, b_{2} being strict NetStr over T st RelStr(# the carrier of b_{1}, the InternalRel of b_{1} #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of b_{1} = f * the mapping of N & RelStr(# the carrier of b_{2}, the InternalRel of b_{2} #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of b_{2} = f * the mapping of N holds

b_{1} = b_{2}
;

end;
let T be 1-sorted ;

let f be Function of S,T;

let N be NetStr over S;

func f * N -> strict NetStr over T means :Def8: :: WAYBEL_9:def 8

( RelStr(# the carrier of it, the InternalRel of it #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of it = f * the mapping of N );

existence ( RelStr(# the carrier of it, the InternalRel of it #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of it = f * the mapping of N );

ex b

( RelStr(# the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def8 defines * WAYBEL_9:def 8 :

for S being non empty 1-sorted

for T being 1-sorted

for f being Function of S,T

for N being NetStr over S

for b_{5} being strict NetStr over T holds

( b_{5} = f * N iff ( RelStr(# the carrier of b_{5}, the InternalRel of b_{5} #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of b_{5} = f * the mapping of N ) );

for S being non empty 1-sorted

for T being 1-sorted

for f being Function of S,T

for N being NetStr over S

for b

( b

registration

let S be non empty 1-sorted ;

let T be 1-sorted ;

let f be Function of S,T;

let N be non empty NetStr over S;

coherence

not f * N is empty

end;
let T be 1-sorted ;

let f be Function of S,T;

let N be non empty NetStr over S;

coherence

not f * N is empty

proof end;

registration

let S be non empty 1-sorted ;

let T be 1-sorted ;

let f be Function of S,T;

let N be reflexive NetStr over S;

coherence

f * N is reflexive

end;
let T be 1-sorted ;

let f be Function of S,T;

let N be reflexive NetStr over S;

coherence

f * N is reflexive

proof end;

registration

let S be non empty 1-sorted ;

let T be 1-sorted ;

let f be Function of S,T;

let N be antisymmetric NetStr over S;

coherence

f * N is antisymmetric

end;
let T be 1-sorted ;

let f be Function of S,T;

let N be antisymmetric NetStr over S;

coherence

f * N is antisymmetric

proof end;

registration

let S be non empty 1-sorted ;

let T be 1-sorted ;

let f be Function of S,T;

let N be transitive NetStr over S;

coherence

f * N is transitive

end;
let T be 1-sorted ;

let f be Function of S,T;

let N be transitive NetStr over S;

coherence

f * N is transitive

proof end;

registration

let S be non empty 1-sorted ;

let T be 1-sorted ;

let f be Function of S,T;

let N be directed NetStr over S;

coherence

f * N is directed

end;
let T be 1-sorted ;

let f be Function of S,T;

let N be directed NetStr over S;

coherence

f * N is directed

proof end;

theorem Th18: :: WAYBEL_9:18

for L being non empty RelStr

for N being non empty NetStr over L

for x being Element of L holds (x "/\") * N = x "/\" N

for N being non empty NetStr over L

for x being Element of L holds (x "/\") * N = x "/\" N

proof end;

theorem :: WAYBEL_9:19

for S, T being TopStruct

for F being Subset-Family of S

for G being Subset-Family of T st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & F = G & F is open holds

G is open

for F being Subset-Family of S

for G being Subset-Family of T st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & F = G & F is open holds

G is open

proof end;

theorem :: WAYBEL_9:20

for S, T being TopStruct

for F being Subset-Family of S

for G being Subset-Family of T st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & F = G & F is closed holds

G is closed

for F being Subset-Family of S

for G being Subset-Family of T st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & F = G & F is closed holds

G is closed

proof end;

definition

attr c_{1} is strict ;

struct TopRelStr -> TopStruct , RelStr ;

aggr TopRelStr(# carrier, InternalRel, topology #) -> TopRelStr ;

end;
struct TopRelStr -> TopStruct , RelStr ;

aggr TopRelStr(# carrier, InternalRel, topology #) -> TopRelStr ;

registration

let A be non empty set ;

let R be Relation of A,A;

let T be Subset-Family of A;

coherence

not TopRelStr(# A,R,T #) is empty ;

end;
let R be Relation of A,A;

let T be Subset-Family of A;

coherence

not TopRelStr(# A,R,T #) is empty ;

registration

let x be set ;

let R be Relation of {x};

let T be Subset-Family of {x};

coherence

TopRelStr(# {x},R,T #) is 1 -element ;

end;
let R be Relation of {x};

let T be Subset-Family of {x};

coherence

TopRelStr(# {x},R,T #) is 1 -element ;

registration

let X be set ;

let O be Order of X;

let T be Subset-Family of X;

coherence

( TopRelStr(# X,O,T #) is reflexive & TopRelStr(# X,O,T #) is transitive & TopRelStr(# X,O,T #) is antisymmetric )

end;
let O be Order of X;

let T be Subset-Family of X;

coherence

( TopRelStr(# X,O,T #) is reflexive & TopRelStr(# X,O,T #) is transitive & TopRelStr(# X,O,T #) is antisymmetric )

proof end;

Lm4: for tau being Subset-Family of {0}

for r being Relation of {0} st tau = {{},{0}} & r = {[0,0]} holds

( TopRelStr(# {0},r,tau #) is reflexive & TopRelStr(# {0},r,tau #) is discrete & TopRelStr(# {0},r,tau #) is finite & TopRelStr(# {0},r,tau #) is 1 -element )

proof end;

registration

existence

ex b_{1} being TopRelStr st

( b_{1} is reflexive & b_{1} is discrete & b_{1} is strict & b_{1} is finite & b_{1} is 1 -element )

end;
ex b

( b

proof end;

definition

mode TopLattice is TopSpace-like reflexive transitive antisymmetric with_suprema with_infima TopRelStr ;

end;
registration

ex b_{1} being TopLattice st

( b_{1} is strict & b_{1} is discrete & b_{1} is finite & b_{1} is compact & b_{1} is Hausdorff & b_{1} is 1 -element )
end;

cluster non empty finite 1 -element TopSpace-like Hausdorff discrete reflexive transitive antisymmetric with_suprema with_infima compact strict for TopRelStr ;

existence ex b

( b

proof end;

registration

let T be non empty Hausdorff TopSpace;

coherence

for b_{1} being non empty SubSpace of T holds b_{1} is Hausdorff
;

end;
coherence

for b

theorem Th21: :: WAYBEL_9:21

for T being non empty TopSpace

for p being Point of T

for A being Element of (OpenNeighborhoods p) holds A is a_neighborhood of p

for p being Point of T

for A being Element of (OpenNeighborhoods p) holds A is a_neighborhood of p

proof end;

theorem Th22: :: WAYBEL_9:22

for T being non empty TopSpace

for p being Point of T

for A, B being Element of (OpenNeighborhoods p) holds A /\ B is Element of (OpenNeighborhoods p)

for p being Point of T

for A, B being Element of (OpenNeighborhoods p) holds A /\ B is Element of (OpenNeighborhoods p)

proof end;

theorem :: WAYBEL_9:23

for T being non empty TopSpace

for p being Point of T

for A, B being Element of (OpenNeighborhoods p) holds A \/ B is Element of (OpenNeighborhoods p)

for p being Point of T

for A, B being Element of (OpenNeighborhoods p) holds A \/ B is Element of (OpenNeighborhoods p)

proof end;

theorem Th24: :: WAYBEL_9:24

for T being non empty TopSpace

for p being Element of T

for N being net of T st p in Lim N holds

for S being Subset of T st S = rng the mapping of N holds

p in Cl S

for p being Element of T

for N being net of T st p in Lim N holds

for S being Subset of T st S = rng the mapping of N holds

p in Cl S

proof end;

theorem Th25: :: WAYBEL_9:25

for T being Hausdorff TopLattice

for N being convergent net of T

for f being Function of T,T st f is continuous holds

f . (lim N) in Lim (f * N)

for N being convergent net of T

for f being Function of T,T st f is continuous holds

f . (lim N) in Lim (f * N)

proof end;

theorem Th26: :: WAYBEL_9:26

for T being Hausdorff TopLattice

for N being convergent net of T

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

x "/\" (lim N) in Lim (x "/\" N)

for N being convergent net of T

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

x "/\" (lim N) in Lim (x "/\" N)

proof end;

theorem Th27: :: WAYBEL_9:27

for S being Hausdorff TopLattice

for x being Element of S st ( for a being Element of S holds a "/\" is continuous ) holds

uparrow x is closed

for x being Element of S st ( for a being Element of S holds a "/\" is continuous ) holds

uparrow x is closed

proof end;

theorem Th28: :: WAYBEL_9:28

for S being Hausdorff compact TopLattice

for x being Element of S st ( for b being Element of S holds b "/\" is continuous ) holds

downarrow x is closed

for x being Element of S st ( for b being Element of S holds b "/\" is continuous ) holds

downarrow x is closed

proof end;

definition

let T be non empty TopSpace;

let N be non empty NetStr over T;

let p be Point of T;

end;
let N be non empty NetStr over T;

let p be Point of T;

pred p is_a_cluster_point_of N means :: WAYBEL_9:def 9

for O being a_neighborhood of p holds N is_often_in O;

for O being a_neighborhood of p holds N is_often_in O;

:: deftheorem defines is_a_cluster_point_of WAYBEL_9:def 9 :

for T being non empty TopSpace

for N being non empty NetStr over T

for p being Point of T holds

( p is_a_cluster_point_of N iff for O being a_neighborhood of p holds N is_often_in O );

for T being non empty TopSpace

for N being non empty NetStr over T

for p being Point of T holds

( p is_a_cluster_point_of N iff for O being a_neighborhood of p holds N is_often_in O );

theorem :: WAYBEL_9:29

for L being non empty TopSpace

for N being net of L

for c being Point of L st c in Lim N holds

c is_a_cluster_point_of N

for N being net of L

for c being Point of L st c in Lim N holds

c is_a_cluster_point_of N

proof end;

theorem Th30: :: WAYBEL_9:30

for T being non empty Hausdorff compact TopSpace

for N being net of T ex c being Point of T st c is_a_cluster_point_of N

for N being net of T ex c being Point of T st c is_a_cluster_point_of N

proof end;

theorem Th31: :: WAYBEL_9:31

for L being non empty TopSpace

for N being net of L

for M being subnet of N

for c being Point of L st c is_a_cluster_point_of M holds

c is_a_cluster_point_of N by YELLOW_6:18;

for N being net of L

for M being subnet of N

for c being Point of L st c is_a_cluster_point_of M holds

c is_a_cluster_point_of N by YELLOW_6:18;

theorem Th32: :: WAYBEL_9:32

for T being non empty TopSpace

for N being net of T

for x being Point of T st x is_a_cluster_point_of N holds

ex M being subnet of N st x in Lim M

for N being net of T

for x being Point of T st x is_a_cluster_point_of N holds

ex M being subnet of N st x in Lim M

proof end;

theorem Th33: :: WAYBEL_9:33

for L being non empty Hausdorff compact TopSpace

for N being net of L st ( for c, d being Point of L st c is_a_cluster_point_of N & d is_a_cluster_point_of N holds

c = d ) holds

for s being Point of L st s is_a_cluster_point_of N holds

s in Lim N

for N being net of L st ( for c, d being Point of L st c is_a_cluster_point_of N & d is_a_cluster_point_of N holds

c = d ) holds

for s being Point of L st s is_a_cluster_point_of N holds

s in Lim N

proof end;

theorem Th34: :: WAYBEL_9:34

for S being non empty TopSpace

for c being Point of S

for N being net of S

for A being Subset of S st c is_a_cluster_point_of N & A is closed & rng the mapping of N c= A holds

c in A

for c being Point of S

for N being net of S

for A being Subset of S st c is_a_cluster_point_of N & A is closed & rng the mapping of N c= A holds

c in A

proof end;

Lm5: for S being Hausdorff compact TopLattice

for N being net of S

for c being Point of S

for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & N is eventually-directed & c is_a_cluster_point_of N holds

d is_>=_than rng the mapping of N

proof end;

Lm6: for S being Hausdorff compact TopLattice

for N being net of S

for c being Point of S

for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & c is_a_cluster_point_of N holds

for b being Element of S st rng the mapping of N is_<=_than b holds

d <= b

proof end;

theorem Th35: :: WAYBEL_9:35

for S being Hausdorff compact TopLattice

for c being Point of S

for N being net of S st ( for x being Element of S holds x "/\" is continuous ) & N is eventually-directed & c is_a_cluster_point_of N holds

c = sup N

for c being Point of S

for N being net of S st ( for x being Element of S holds x "/\" is continuous ) & N is eventually-directed & c is_a_cluster_point_of N holds

c = sup N

proof end;

Lm7: for S being Hausdorff compact TopLattice

for N being net of S

for c being Point of S

for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & N is eventually-filtered & c is_a_cluster_point_of N holds

d is_<=_than rng the mapping of N

proof end;

Lm8: for S being Hausdorff compact TopLattice

for N being net of S

for c being Point of S

for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & c is_a_cluster_point_of N holds

for b being Element of S st rng the mapping of N is_>=_than b holds

d >= b

proof end;

theorem Th36: :: WAYBEL_9:36

for S being Hausdorff compact TopLattice

for c being Point of S

for N being net of S st ( for x being Element of S holds x "/\" is continuous ) & N is eventually-filtered & c is_a_cluster_point_of N holds

c = inf N

for c being Point of S

for N being net of S st ( for x being Element of S holds x "/\" is continuous ) & N is eventually-filtered & c is_a_cluster_point_of N holds

c = inf N

proof end;

:: Proposition 4.4 s. 32 (i) & (ii) => MC

theorem Th37: :: WAYBEL_9:37

for S being Hausdorff TopLattice st ( for N being net of S st N is eventually-directed holds

( ex_sup_of N & sup N in Lim N ) ) & ( for x being Element of S holds x "/\" is continuous ) holds

S is meet-continuous

( ex_sup_of N & sup N in Lim N ) ) & ( for x being Element of S holds x "/\" is continuous ) holds

S is meet-continuous

proof end;

:: Proposition 4.4 s. 32 (ii) => (i)

theorem Th38: :: WAYBEL_9:38

for S being Hausdorff compact TopLattice st ( for x being Element of S holds x "/\" is continuous ) holds

for N being net of S st N is eventually-directed holds

( ex_sup_of N & sup N in Lim N )

for N being net of S st N is eventually-directed holds

( ex_sup_of N & sup N in Lim N )

proof end;

:: Proposition 4.4 s. 32 (ii) => (i) dual

theorem Th39: :: WAYBEL_9:39

for S being Hausdorff compact TopLattice st ( for x being Element of S holds x "/\" is continuous ) holds

for N being net of S st N is eventually-filtered holds

( ex_inf_of N & inf N in Lim N )

for N being net of S st N is eventually-filtered holds

( ex_inf_of N & inf N in Lim N )

proof end;

theorem :: WAYBEL_9:40

for S being Hausdorff compact TopLattice st ( for x being Element of S holds x "/\" is continuous ) holds

S is bounded

S is bounded

proof end;

theorem :: WAYBEL_9:41

for S being Hausdorff compact TopLattice st ( for x being Element of S holds x "/\" is continuous ) holds

S is meet-continuous

S is meet-continuous

proof end;

:: Acknowledgements:

:: =================

::

:: I would like to thank Professor A. Trybulec for his help in the preparation

:: of the article.

::-------------------------------------------------------------------