:: WAYBEL_9 semantic presentation

registration

let L be non empty RelStr ;
cluster id L -> monotone ;
coherence by YELLOW_2:13;

end;

definition

let S, T be non empty RelStr ;
let f be Function of S,T;
redefine attr f is antitone means :Def1: :: WAYBEL_9:def 1
for x, y being Element of S st x <= y holds
f . x >= f . y;
compatibility

proof end;

end;

:: deftheorem Def1 defines antitone WAYBEL_9:def 1 :

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

proof end;

theorem Th2: :: WAYBEL_9:2

proof end;

theorem Th3: :: 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_a_cover_of A holds
G is_a_cover_of B

proof end;

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)

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)

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}

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

proof end;

theorem Th8: :: WAYBEL_9:8

for T being non empty 1-sorted
for N being non empty NetStr of 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;
cluster NetStr(# D,(the InternalRel of L |_2 D),n #) -> directed ;
coherence by WAYBEL_2:19;

end;

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;
cluster NetStr(# D,(the InternalRel of L |_2 D),n #) -> transitive directed ;
coherence by Lm3;

end;

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

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

proof end;

definition

let L be non empty RelStr ;
let x be Element of L;
let N be net of L;
:: original: "/\"
redefine func x "/\" N -> strict net of L;
coherence by Th10;

end;

registration

let L be non empty RelStr ;
let x be Element of L;
let N be non empty reflexive NetStr of L;
cluster x "/\" N -> reflexive ;
coherence

proof end;

end;

registration

let L be non empty RelStr ;
let x be Element of L;
let N be non empty antisymmetric NetStr of L;
cluster x "/\" N -> antisymmetric ;
coherence

proof end;

end;

registration

let L be non empty RelStr ;
let x be Element of L;
let N be non empty transitive NetStr of L;
cluster x "/\" N -> transitive ;
coherence

proof end;

end;

registration

let L be non empty RelStr ;
let J be set ;
let f be Function of J,the carrier of L;
cluster FinSups f -> transitive ;
coherence

proof end;

end;

definition

let L be non empty RelStr ;
let N be NetStr of L;
func inf N -> Element of L equals :: WAYBEL_9:def 2
Inf ;
coherence ;

end;

:: deftheorem defines inf WAYBEL_9:def 2 :

definition

let L be RelStr ;
let N be NetStr of L;
pred ex_sup_of N means :Def3: :: WAYBEL_9:def 3
ex_sup_of rng the mapping of N,L;
pred ex_inf_of N means :Def4: :: WAYBEL_9:def 4
ex_inf_of rng the mapping of N,L;

end;

:: deftheorem Def3 defines ex_sup_of WAYBEL_9:def 3 :

:: deftheorem Def4 defines ex_inf_of WAYBEL_9:def 4 :

definition

let L be RelStr ;
func L +id -> strict NetStr of 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

proof end;

uniqueness ;

end;

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

registration

let L be non empty RelStr ;
cluster L +id -> non empty strict ;
coherence

proof end;

end;

registration

let L be reflexive RelStr ;
cluster L +id -> reflexive strict ;
coherence

proof end;

end;

registration

let L be antisymmetric RelStr ;
cluster L +id -> antisymmetric strict ;
coherence

proof end;

end;

registration

let L be transitive RelStr ;
cluster L +id -> transitive strict ;
coherence

proof end;

end;

registration

let L be with_suprema RelStr ;
cluster L +id -> non empty strict directed ;
coherence

proof end;

end;

registration

let L be directed RelStr ;
cluster L +id -> strict directed ;
coherence

proof end;

end;

registration

let L be non empty RelStr ;
cluster L +id -> non empty strict monotone eventually-directed ;
coherence

proof end;

end;

definition

let L be RelStr ;
func L opp+id -> strict NetStr of 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

proof end;

uniqueness ;

end;

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

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 ;
cluster L opp+id -> non empty strict ;
coherence

proof end;

end;

registration

let L be reflexive RelStr ;
cluster L opp+id -> reflexive strict ;
coherence

proof end;

end;

registration

let L be antisymmetric RelStr ;
cluster L opp+id -> antisymmetric strict ;
coherence

proof end;

end;

registration

let L be transitive RelStr ;
cluster L opp+id -> transitive strict ;
coherence

proof end;

end;

registration

let L be with_infima RelStr ;
cluster L opp+id -> non empty strict directed ;
coherence

proof end;

end;

registration

let L be non empty RelStr ;
cluster L opp+id -> non empty strict antitone eventually-filtered ;
coherence

proof end;

end;

definition

let L be non empty 1-sorted ;
let N be non empty NetStr of L;
let i be Element of N;
func N | i -> strict NetStr of L means :Def7: :: WAYBEL_9:def 7
( ( for x being set 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines | WAYBEL_9:def 7 :

theorem :: WAYBEL_9:12

for L being non empty 1-sorted
for N being non empty NetStr of 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 of 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 of 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 of L;
let i be Element of N;
cluster N | i -> non empty reflexive strict ;
coherence

proof end;

end;

registration

let L be non empty 1-sorted ;
let N be non empty directed NetStr of L;
let i be Element of N;
cluster N | i -> non empty strict ;
coherence

proof end;

end;

registration

let L be non empty 1-sorted ;
let N be non empty reflexive antisymmetric NetStr of L;
let i be Element of N;
cluster N | i -> non empty reflexive antisymmetric strict ;
coherence

proof end;

end;

registration

let L be non empty 1-sorted ;
let N be non empty antisymmetric directed NetStr of L;
let i be Element of N;
cluster N | i -> non empty antisymmetric strict ;
coherence

proof end;

end;

registration

let L be non empty 1-sorted ;
let N be non empty reflexive transitive NetStr of L;
let i be Element of N;
cluster N | i -> non empty reflexive transitive strict ;
coherence

proof end;

end;

registration

let L be non empty 1-sorted ;
let N be net of L;
let i be Element of N;
cluster N | i -> non empty transitive strict directed ;
coherence

proof end;

end;

theorem :: WAYBEL_9:15

for L being non empty 1-sorted
for N being non empty reflexive NetStr of 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 of 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

proof end;

registration

let T be non empty 1-sorted ;
let N be net of T;
cluster strict subnet of N;
existence

proof end;

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 by Th17;

end;

definition

let S be non empty 1-sorted ;
let T be 1-sorted ;
let f be Function of S,T;
let N be NetStr of S;
func f * N -> strict NetStr of 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

proof end;

uniqueness ;

end;

:: deftheorem Def8 defines * WAYBEL_9:def 8 :

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 of S;
cluster f * N -> non empty strict ;
coherence

proof end;

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 of S;
cluster f * N -> reflexive strict ;
coherence

proof end;

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 of S;
cluster f * N -> antisymmetric strict ;
coherence

proof end;

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 of S;
cluster f * N -> transitive strict ;
coherence

proof end;

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 of S;
cluster f * N -> strict directed ;
coherence

proof end;

end;

theorem Th18: :: WAYBEL_9:18

for L being non empty RelStr
for N being non empty NetStr of L
for x being Element of L holds (x "/\" ) * N = x "/\" N

proof end;

theorem Th19: :: 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

proof end;

theorem :: WAYBEL_9:20

proof end;

definition

attr c₁ is strict;
struct TopRelStr -> TopStruct , RelStr ;
aggr TopRelStr(# carrier, InternalRel, topology #) -> TopRelStr ;

end;

registration

let A be non empty set ;
let R be Relation of A,A;
let T be Subset-Family of A;
cluster TopRelStr(# A,R,T #) -> non empty ;
coherence

proof end;

end;

registration

let x be set ;
let R be Relation of {x};
let T be Subset-Family of {x};
cluster TopRelStr(# {x},R,T #) -> non empty trivial ;
coherence

proof end;

end;

registration

let X be set ;
let O be Order of X;
let T be Subset-Family of X;
cluster TopRelStr(# X,O,T #) -> reflexive transitive antisymmetric ;
coherence

proof end;

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 trivial & TopRelStr(# {0},r,tau #) is reflexive & not TopRelStr(# {0},r,tau #) is empty & TopRelStr(# {0},r,tau #) is discrete & TopRelStr(# {0},r,tau #) is finite )

proof end;

registration

cluster non empty reflexive discrete finite trivial strict TopRelStr ;
existence

proof end;

end;

definition

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

end;

registration

cluster non empty compact Hausdorff discrete finite trivial strict TopRelStr ;
existence

proof end;

end;

registration

let T be non empty Hausdorff TopSpace;
cluster non empty -> non empty Hausdorff SubSpace of T;
coherence by TOPMETR:3;

end;

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

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)

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)

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

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)

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)

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

proof end;

theorem Th28: :: WAYBEL_9:28

for S being compact Hausdorff TopLattice
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 of T;
let p be Point of T;
pred p is_a_cluster_point_of N means :Def9: :: WAYBEL_9:def 9
for O being a_neighborhood of p holds N is_often_in O;

end;

:: deftheorem Def9 defines is_a_cluster_point_of WAYBEL_9:def 9 :

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

proof end;

theorem Th30: :: WAYBEL_9:30

for T being non empty compact Hausdorff TopSpace
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

proof end;

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

proof end;

theorem Th33: :: WAYBEL_9:33

for L being non empty compact Hausdorff 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

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

proof end;

Lm5: for S being compact Hausdorff 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 compact Hausdorff 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 compact Hausdorff 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

proof end;

Lm7: for S being compact Hausdorff 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 compact Hausdorff 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 compact Hausdorff 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

proof end;

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

proof end;

theorem Th38: :: WAYBEL_9:38

for S being compact Hausdorff 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 )

proof end;

theorem Th39: :: WAYBEL_9:39

for S being compact Hausdorff 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 )

proof end;

theorem :: WAYBEL_9:40

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

proof end;

theorem :: WAYBEL_9:41

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

proof end;