:: by Czes{\l}aw Byli\'nski and Piotr Rudnicki

::

:: Received August 27, 1997

:: Copyright (c) 1997-2021 Association of Mizar Users

theorem Th1: :: WAYBEL14:1

for X being set

for F being finite Subset-Family of X ex G being finite Subset-Family of X st

( G c= F & union G = union F & ( for g being Subset of X st g in G holds

not g c= union (G \ {g}) ) )

for F being finite Subset-Family of X ex G being finite Subset-Family of X st

( G c= F & union G = union F & ( for g being Subset of X st g in G holds

not g c= union (G \ {g}) ) )

proof end;

Lm1: for S being 1-sorted

for X, Y being Subset of S holds

( X c= Y ` iff Y c= X ` )

proof end;

theorem Th3: :: WAYBEL14:3

for R being non empty transitive antisymmetric with_infima RelStr

for x, y being Element of R holds downarrow (x "/\" y) = (downarrow x) /\ (downarrow y)

for x, y being Element of R holds downarrow (x "/\" y) = (downarrow x) /\ (downarrow y)

proof end;

theorem :: WAYBEL14:4

for R being non empty transitive antisymmetric with_suprema RelStr

for x, y being Element of R holds uparrow (x "\/" y) = (uparrow x) /\ (uparrow y)

for x, y being Element of R holds uparrow (x "\/" y) = (uparrow x) /\ (uparrow y)

proof end;

theorem Th5: :: WAYBEL14:5

for L being non empty antisymmetric complete RelStr

for X being lower Subset of L st sup X in X holds

X = downarrow (sup X)

for X being lower Subset of L st sup X in X holds

X = downarrow (sup X)

proof end;

theorem :: WAYBEL14:6

for L being non empty antisymmetric complete RelStr

for X being upper Subset of L st inf X in X holds

X = uparrow (inf X)

for X being upper Subset of L st inf X in X holds

X = uparrow (inf X)

proof end;

theorem Th7: :: WAYBEL14:7

for R being non empty reflexive transitive RelStr

for x, y being Element of R holds

( x << y iff uparrow y c= wayabove x )

for x, y being Element of R holds

( x << y iff uparrow y c= wayabove x )

proof end;

theorem :: WAYBEL14:8

for R being non empty reflexive transitive RelStr

for x, y being Element of R holds

( x << y iff downarrow x c= waybelow y )

for x, y being Element of R holds

( x << y iff downarrow x c= waybelow y )

proof end;

theorem Th9: :: WAYBEL14:9

for R being non empty reflexive antisymmetric complete RelStr

for x being Element of R holds

( sup (waybelow x) <= x & x <= inf (wayabove x) )

for x being Element of R holds

( sup (waybelow x) <= x & x <= inf (wayabove x) )

proof end;

theorem Th10: :: WAYBEL14:10

for L being non empty antisymmetric lower-bounded RelStr holds uparrow (Bottom L) = the carrier of L

proof end;

theorem Th12: :: WAYBEL14:12

for P being with_suprema Poset

for x, y being Element of P holds (wayabove x) "\/" (wayabove y) c= uparrow (x "\/" y)

for x, y being Element of P holds (wayabove x) "\/" (wayabove y) c= uparrow (x "\/" y)

proof end;

theorem :: WAYBEL14:13

for P being with_infima Poset

for x, y being Element of P holds (waybelow x) "/\" (waybelow y) c= downarrow (x "/\" y)

for x, y being Element of P holds (waybelow x) "/\" (waybelow y) c= downarrow (x "/\" y)

proof end;

theorem Th14: :: WAYBEL14:14

for R being non empty with_suprema Poset

for l being Element of R holds

( l is co-prime iff for x, y being Element of R holds

( not l <= x "\/" y or l <= x or l <= y ) )

for l being Element of R holds

( l is co-prime iff for x, y being Element of R holds

( not l <= x "\/" y or l <= x or l <= y ) )

proof end;

theorem Th15: :: WAYBEL14:15

for P being non empty complete Poset

for V being non empty Subset of P holds downarrow (inf V) = meet { (downarrow u) where u is Element of P : u in V }

for V being non empty Subset of P holds downarrow (inf V) = meet { (downarrow u) where u is Element of P : u in V }

proof end;

theorem :: WAYBEL14:16

for P being non empty complete Poset

for V being non empty Subset of P holds uparrow (sup V) = meet { (uparrow u) where u is Element of P : u in V }

for V being non empty Subset of P holds uparrow (sup V) = meet { (uparrow u) where u is Element of P : u in V }

proof end;

registration
end;

theorem Th17: :: WAYBEL14:17

for T being non empty TopSpace

for S being irreducible Subset of T

for V being Element of (InclPoset the topology of T) st V = S ` holds

V is prime

for S being irreducible Subset of T

for V being Element of (InclPoset the topology of T) st V = S ` holds

V is prime

proof end;

theorem Th18: :: WAYBEL14:18

for T being non empty TopSpace

for x, y being Element of (InclPoset the topology of T) holds

( x "\/" y = x \/ y & x "/\" y = x /\ y )

for x, y being Element of (InclPoset the topology of T) holds

( x "\/" y = x \/ y & x "/\" y = x /\ y )

proof end;

theorem Th19: :: WAYBEL14:19

for T being non empty TopSpace

for V being Element of (InclPoset the topology of T) holds

( V is prime iff for X, Y being Element of (InclPoset the topology of T) holds

( not X /\ Y c= V or X c= V or Y c= V ) )

for V being Element of (InclPoset the topology of T) holds

( V is prime iff for X, Y being Element of (InclPoset the topology of T) holds

( not X /\ Y c= V or X c= V or Y c= V ) )

proof end;

theorem :: WAYBEL14:20

for T being non empty TopSpace

for V being Element of (InclPoset the topology of T) holds

( V is co-prime iff for X, Y being Element of (InclPoset the topology of T) holds

( not V c= X \/ Y or V c= X or V c= Y ) )

for V being Element of (InclPoset the topology of T) holds

( V is co-prime iff for X, Y being Element of (InclPoset the topology of T) holds

( not V c= X \/ Y or V c= X or V c= Y ) )

proof end;

registration
end;

theorem Th21: :: WAYBEL14:21

for T being non empty TopSpace

for L being TopLattice

for t being Point of T

for l being Point of L

for X being Subset-Family of L st TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of L, the topology of L #) & t = l & X is Basis of l holds

X is Basis of t

for L being TopLattice

for t being Point of T

for l being Point of L

for X being Subset-Family of L st TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of L, the topology of L #) & t = l & X is Basis of l holds

X is Basis of t

proof end;

theorem Th22: :: WAYBEL14:22

for L being TopLattice

for x being Element of L st ( for X being Subset of L st X is open holds

X is upper ) holds

uparrow x is compact

for x being Element of L st ( for X being Subset of L st X is open holds

X is upper ) holds

uparrow x is compact

proof end;

registration
end;

Lm2: for L being complete Scott TopLattice

for V being filtered Subset of L

for F being Subset-Family of L

for CF being Subset of (InclPoset (sigma L)) st F = { (downarrow u) where u is Element of L : u in V } & CF = COMPLEMENT F holds

CF is directed

proof end;

theorem Th25: :: WAYBEL14:25

for L being complete Scott TopLattice

for VV being Subset of (InclPoset (sigma L))

for X being filtered Subset of L st VV = { ((downarrow x) `) where x is Element of L : x in X } holds

VV is directed

for VV being Subset of (InclPoset (sigma L))

for X being filtered Subset of L st VV = { ((downarrow x) `) where x is Element of L : x in X } holds

VV is directed

proof end;

theorem Th26: :: WAYBEL14:26

for L being complete Scott TopLattice

for x being Element of L

for X being Subset of L st X is open & x in X holds

inf X << x

for x being Element of L

for X being Subset of L st X is open & x in X holds

inf X << x

proof end;

:: p. 105

definition

let R be non empty reflexive RelStr ;

let f be Function of [:R,R:],R;

end;
let f be Function of [:R,R:],R;

attr f is jointly_Scott-continuous means :: WAYBEL14:def 1

for T being non empty TopSpace st TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence R) holds

ex ft being Function of [:T,T:],T st

( ft = f & ft is continuous );

for T being non empty TopSpace st TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence R) holds

ex ft being Function of [:T,T:],T st

( ft = f & ft is continuous );

:: deftheorem defines jointly_Scott-continuous WAYBEL14:def 1 :

for R being non empty reflexive RelStr

for f being Function of [:R,R:],R holds

( f is jointly_Scott-continuous iff for T being non empty TopSpace st TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence R) holds

ex ft being Function of [:T,T:],T st

( ft = f & ft is continuous ) );

for R being non empty reflexive RelStr

for f being Function of [:R,R:],R holds

( f is jointly_Scott-continuous iff for T being non empty TopSpace st TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence R) holds

ex ft being Function of [:T,T:],T st

( ft = f & ft is continuous ) );

theorem Th27: :: WAYBEL14:27

for L being complete Scott TopLattice

for X being Subset of L

for V being Element of (InclPoset (sigma L)) st V = X holds

( V is co-prime iff ( X is filtered & X is upper ) )

for X being Subset of L

for V being Element of (InclPoset (sigma L)) st V = X holds

( V is co-prime iff ( X is filtered & X is upper ) )

proof end;

theorem :: WAYBEL14:28

for L being complete Scott TopLattice

for X being Subset of L

for V being Element of (InclPoset (sigma L)) st V = X & ex x being Element of L st X = (downarrow x) ` holds

( V is prime & V <> the carrier of L )

for X being Subset of L

for V being Element of (InclPoset (sigma L)) st V = X & ex x being Element of L st X = (downarrow x) ` holds

( V is prime & V <> the carrier of L )

proof end;

theorem Th29: :: WAYBEL14:29

for L being complete Scott TopLattice

for X being Subset of L

for V being Element of (InclPoset (sigma L)) st V = X & sup_op L is jointly_Scott-continuous & V is prime & V <> the carrier of L holds

ex x being Element of L st X = (downarrow x) `

for X being Subset of L

for V being Element of (InclPoset (sigma L)) st V = X & sup_op L is jointly_Scott-continuous & V is prime & V <> the carrier of L holds

ex x being Element of L st X = (downarrow x) `

proof end;

theorem :: WAYBEL14:32

for L being complete Scott TopLattice st L is continuous holds

( L is compact & L is locally-compact & L is sober & L is Baire )

( L is compact & L is locally-compact & L is sober & L is Baire )

proof end;

theorem Th33: :: WAYBEL14:33

for L being complete Scott TopLattice

for X being Subset of L st L is continuous & X in sigma L holds

X = union { (wayabove x) where x is Element of L : x in X }

for X being Subset of L st L is continuous & X in sigma L holds

X = union { (wayabove x) where x is Element of L : x in X }

proof end;

theorem :: WAYBEL14:34

for L being complete Scott TopLattice st ( for X being Subset of L st X in sigma L holds

X = union { (wayabove x) where x is Element of L : x in X } ) holds

L is continuous

X = union { (wayabove x) where x is Element of L : x in X } ) holds

L is continuous

proof end;

theorem :: WAYBEL14:35

for L being complete Scott TopLattice

for x being Element of L st L is continuous holds

ex B being Basis of x st

for X being Subset of L st X in B holds

( X is open & X is filtered )

for x being Element of L st L is continuous holds

ex B being Basis of x st

for X being Subset of L st X in B holds

( X is open & X is filtered )

proof end;

theorem Th37: :: WAYBEL14:37

for L being complete Scott TopLattice

for x being Element of L st ( for x being Element of L ex B being Basis of x st

for Y being Subset of L st Y in B holds

( Y is open & Y is filtered ) ) & InclPoset (sigma L) is continuous holds

x = "\/" ( { (inf X) where X is Subset of L : ( x in X & X in sigma L ) } ,L)

for x being Element of L st ( for x being Element of L ex B being Basis of x st

for Y being Subset of L st Y in B holds

( Y is open & Y is filtered ) ) & InclPoset (sigma L) is continuous holds

x = "\/" ( { (inf X) where X is Subset of L : ( x in X & X in sigma L ) } ,L)

proof end;

theorem Th38: :: WAYBEL14:38

for L being complete Scott TopLattice st ( for x being Element of L holds x = "\/" ( { (inf X) where X is Subset of L : ( x in X & X in sigma L ) } ,L) ) holds

L is continuous

L is continuous

proof end;

theorem Th39: :: WAYBEL14:39

for L being complete Scott TopLattice holds

( ( for x being Element of L ex B being Basis of x st

for Y being Subset of L st Y in B holds

( Y is open & Y is filtered ) ) iff for V being Element of (InclPoset (sigma L)) ex VV being Subset of (InclPoset (sigma L)) st

( V = sup VV & ( for W being Element of (InclPoset (sigma L)) st W in VV holds

W is co-prime ) ) )

( ( for x being Element of L ex B being Basis of x st

for Y being Subset of L st Y in B holds

( Y is open & Y is filtered ) ) iff for V being Element of (InclPoset (sigma L)) ex VV being Subset of (InclPoset (sigma L)) st

( V = sup VV & ( for W being Element of (InclPoset (sigma L)) st W in VV holds

W is co-prime ) ) )

proof end;

theorem :: WAYBEL14:40

for L being complete Scott TopLattice holds

( ( ( for V being Element of (InclPoset (sigma L)) ex VV being Subset of (InclPoset (sigma L)) st

( V = sup VV & ( for W being Element of (InclPoset (sigma L)) st W in VV holds

W is co-prime ) ) ) & InclPoset (sigma L) is continuous ) iff InclPoset (sigma L) is completely-distributive )

( ( ( for V being Element of (InclPoset (sigma L)) ex VV being Subset of (InclPoset (sigma L)) st

( V = sup VV & ( for W being Element of (InclPoset (sigma L)) st W in VV holds

W is co-prime ) ) ) & InclPoset (sigma L) is continuous ) iff InclPoset (sigma L) is completely-distributive )

proof end;

theorem :: WAYBEL14:41

for L being complete Scott TopLattice holds

( InclPoset (sigma L) is completely-distributive iff ( InclPoset (sigma L) is continuous & (InclPoset (sigma L)) opp is continuous ) )

( InclPoset (sigma L) is completely-distributive iff ( InclPoset (sigma L) is continuous & (InclPoset (sigma L)) opp is continuous ) )

proof end;

theorem :: WAYBEL14:42

for L being complete Scott TopLattice st L is algebraic holds

ex B being Basis of L st B = { (uparrow x) where x is Element of L : x in the carrier of (CompactSublatt L) }

ex B being Basis of L st B = { (uparrow x) where x is Element of L : x in the carrier of (CompactSublatt L) }

proof end;

theorem :: WAYBEL14:43

for L being complete Scott TopLattice st ex B being Basis of L st B = { (uparrow x) where x is Element of L : x in the carrier of (CompactSublatt L) } holds

( InclPoset (sigma L) is algebraic & ( for V being Element of (InclPoset (sigma L)) ex VV being Subset of (InclPoset (sigma L)) st

( V = sup VV & ( for W being Element of (InclPoset (sigma L)) st W in VV holds

W is co-prime ) ) ) )

( InclPoset (sigma L) is algebraic & ( for V being Element of (InclPoset (sigma L)) ex VV being Subset of (InclPoset (sigma L)) st

( V = sup VV & ( for W being Element of (InclPoset (sigma L)) st W in VV holds

W is co-prime ) ) ) )

proof end;

theorem :: WAYBEL14:44

for L being complete Scott TopLattice st InclPoset (sigma L) is algebraic & ( for V being Element of (InclPoset (sigma L)) ex VV being Subset of (InclPoset (sigma L)) st

( V = sup VV & ( for W being Element of (InclPoset (sigma L)) st W in VV holds

W is co-prime ) ) ) holds

ex B being Basis of L st B = { (uparrow x) where x is Element of L : x in the carrier of (CompactSublatt L) }

( V = sup VV & ( for W being Element of (InclPoset (sigma L)) st W in VV holds

W is co-prime ) ) ) holds

ex B being Basis of L st B = { (uparrow x) where x is Element of L : x in the carrier of (CompactSublatt L) }

proof end;

theorem :: WAYBEL14:45

for L being complete Scott TopLattice st ex B being Basis of L st B = { (uparrow x) where x is Element of L : x in the carrier of (CompactSublatt L) } holds

L is algebraic

L is algebraic

proof end;