:: by Robert Milewski

::

:: Received March 4, 1997

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

theorem Th1: :: WAYBEL13:1

for L being non empty reflexive transitive RelStr

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

compactbelow x c= compactbelow y

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

compactbelow x c= compactbelow y

proof end;

theorem Th2: :: WAYBEL13:2

for L being non empty reflexive RelStr

for x being Element of L holds compactbelow x is Subset of (CompactSublatt L)

for x being Element of L holds compactbelow x is Subset of (CompactSublatt L)

proof end;

theorem Th5: :: WAYBEL13:5

for L1 being non empty reflexive antisymmetric lower-bounded RelStr

for L2 being non empty reflexive antisymmetric RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is up-complete holds

the carrier of (CompactSublatt L1) = the carrier of (CompactSublatt L2)

for L2 being non empty reflexive antisymmetric RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is up-complete holds

the carrier of (CompactSublatt L1) = the carrier of (CompactSublatt L2)

proof end;

theorem Th7: :: WAYBEL13:7

for X, E being set

for L being CLSubFrame of BoolePoset X holds

( E in the carrier of (CompactSublatt L) iff ex F being Element of (BoolePoset X) st

( F is finite & E = meet { Y where Y is Element of L : F c= Y } & F c= E ) )

for L being CLSubFrame of BoolePoset X holds

( E in the carrier of (CompactSublatt L) iff ex F being Element of (BoolePoset X) st

( F is finite & E = meet { Y where Y is Element of L : F c= Y } & F c= E ) )

proof end;

theorem Th8: :: WAYBEL13:8

for L being lower-bounded sup-Semilattice holds InclPoset (Ids L) is CLSubFrame of BoolePoset the carrier of L

proof end;

registration

let L be non empty reflexive transitive RelStr ;

existence

ex b_{1} being Ideal of L st b_{1} is principal

end;
existence

ex b

proof end;

theorem Th9: :: WAYBEL13:9

for L being lower-bounded sup-Semilattice

for X being non empty directed Subset of (InclPoset (Ids L)) holds sup X = union X

for X being non empty directed Subset of (InclPoset (Ids L)) holds sup X = union X

proof end;

theorem Th11: :: WAYBEL13:11

for S being lower-bounded sup-Semilattice

for x being Element of (InclPoset (Ids S)) holds

( x is compact iff x is principal Ideal of S )

for x being Element of (InclPoset (Ids S)) holds

( x is compact iff x is principal Ideal of S )

proof end;

theorem Th12: :: WAYBEL13:12

for S being lower-bounded sup-Semilattice

for x being Element of (InclPoset (Ids S)) holds

( x is compact iff ex a being Element of S st x = downarrow a )

for x being Element of (InclPoset (Ids S)) holds

( x is compact iff ex a being Element of S st x = downarrow a )

proof end;

theorem :: WAYBEL13:13

for L being lower-bounded sup-Semilattice

for f being Function of L,(CompactSublatt (InclPoset (Ids L))) st ( for x being Element of L holds f . x = downarrow x ) holds

f is isomorphic

for f being Function of L,(CompactSublatt (InclPoset (Ids L))) st ( for x being Element of L holds f . x = downarrow x ) holds

f is isomorphic

proof end;

theorem Th16: :: WAYBEL13:16

for L being lower-bounded algebraic sup-Semilattice

for f being Function of L,(InclPoset (Ids (CompactSublatt L))) st ( for x being Element of L holds f . x = compactbelow x ) holds

f is isomorphic

for f being Function of L,(InclPoset (Ids (CompactSublatt L))) st ( for x being Element of L holds f . x = compactbelow x ) holds

f is isomorphic

proof end;

theorem :: WAYBEL13:17

for L being lower-bounded algebraic sup-Semilattice

for x being Element of L holds

( compactbelow x is principal Ideal of (CompactSublatt L) iff x is compact )

for x being Element of L holds

( compactbelow x is principal Ideal of (CompactSublatt L) iff x is compact )

proof end;

theorem Th18: :: WAYBEL13:18

for L1, L2 being non empty RelStr

for X being Subset of L1

for x being Element of L1

for f being Function of L1,L2 st f is isomorphic holds

( x is_<=_than X iff f . x is_<=_than f .: X )

for X being Subset of L1

for x being Element of L1

for f being Function of L1,L2 st f is isomorphic holds

( x is_<=_than X iff f . x is_<=_than f .: X )

proof end;

theorem Th19: :: WAYBEL13:19

for L1, L2 being non empty RelStr

for X being Subset of L1

for x being Element of L1

for f being Function of L1,L2 st f is isomorphic holds

( x is_>=_than X iff f . x is_>=_than f .: X )

for X being Subset of L1

for x being Element of L1

for f being Function of L1,L2 st f is isomorphic holds

( x is_>=_than X iff f . x is_>=_than f .: X )

proof end;

theorem Th20: :: WAYBEL13:20

for L1, L2 being non empty antisymmetric RelStr

for f being Function of L1,L2 st f is isomorphic holds

( f is infs-preserving & f is sups-preserving )

for f being Function of L1,L2 st f is isomorphic holds

( f is infs-preserving & f is sups-preserving )

proof end;

registration

let L1, L2 be non empty antisymmetric RelStr ;

for b_{1} being Function of L1,L2 st b_{1} is isomorphic holds

( b_{1} is infs-preserving & b_{1} is sups-preserving )
by Th20;

end;
cluster Function-like V21( the carrier of L1, the carrier of L2) isomorphic -> infs-preserving sups-preserving for Element of K32(K33( the carrier of L1, the carrier of L2));

coherence for b

( b

theorem Th21: :: WAYBEL13:21

for L1, L2, L3 being non empty transitive antisymmetric RelStr

for f being Function of L1,L2 st f is infs-preserving & L2 is full infs-inheriting SubRelStr of L3 & L3 is complete holds

ex g being Function of L1,L3 st

( f = g & g is infs-preserving )

for f being Function of L1,L2 st f is infs-preserving & L2 is full infs-inheriting SubRelStr of L3 & L3 is complete holds

ex g being Function of L1,L3 st

( f = g & g is infs-preserving )

proof end;

theorem Th22: :: WAYBEL13:22

for L1, L2, L3 being non empty transitive antisymmetric RelStr

for f being Function of L1,L2 st f is monotone & f is directed-sups-preserving & L2 is full directed-sups-inheriting SubRelStr of L3 & L3 is complete holds

ex g being Function of L1,L3 st

( f = g & g is directed-sups-preserving )

for f being Function of L1,L2 st f is monotone & f is directed-sups-preserving & L2 is full directed-sups-inheriting SubRelStr of L3 & L3 is complete holds

ex g being Function of L1,L3 st

( f = g & g is directed-sups-preserving )

proof end;

theorem Th23: :: WAYBEL13:23

for L being lower-bounded sup-Semilattice holds InclPoset (Ids (CompactSublatt L)) is CLSubFrame of BoolePoset the carrier of (CompactSublatt L)

proof end;

theorem Th24: :: WAYBEL13:24

for L being lower-bounded algebraic LATTICE ex g being Function of L,(BoolePoset the carrier of (CompactSublatt L)) st

( g is infs-preserving & g is directed-sups-preserving & g is V13() & ( for x being Element of L holds g . x = compactbelow x ) )

( g is infs-preserving & g is directed-sups-preserving & g is V13() & ( for x being Element of L holds g . x = compactbelow x ) )

proof end;

theorem :: WAYBEL13:25

for I being non empty set

for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is lower-bounded algebraic LATTICE ) holds

product J is lower-bounded algebraic LATTICE

for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is lower-bounded algebraic LATTICE ) holds

product J is lower-bounded algebraic LATTICE

proof end;

Lm1: for L being lower-bounded LATTICE st L is algebraic holds

ex X being non empty set ex S being full SubRelStr of BoolePoset X st

( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic )

proof end;

theorem Th26: :: WAYBEL13:26

for L1, L2 being non empty RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds

L1,L2 are_isomorphic

L1,L2 are_isomorphic

proof end;

Lm2: for L being LATTICE st ex X being non empty set ex S being full SubRelStr of BoolePoset X st

( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) holds

ex X being non empty set ex c being closure Function of (BoolePoset X),(BoolePoset X) st

( c is directed-sups-preserving & L, Image c are_isomorphic )

proof end;

Lm3: for L being LATTICE st ex X being set ex S being full SubRelStr of BoolePoset X st

( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) holds

ex X being set ex c being closure Function of (BoolePoset X),(BoolePoset X) st

( c is directed-sups-preserving & L, Image c are_isomorphic )

proof end;

Lm4: for L1, L2 being non empty up-complete Poset

for f being Function of L1,L2 st f is isomorphic holds

for x, y being Element of L1 st x << y holds

f . x << f . y

proof end;

theorem Th27: :: WAYBEL13:27

for L1, L2 being non empty up-complete Poset

for f being Function of L1,L2 st f is isomorphic holds

for x, y being Element of L1 holds

( x << y iff f . x << f . y )

for f being Function of L1,L2 st f is isomorphic holds

for x, y being Element of L1 holds

( x << y iff f . x << f . y )

proof end;

theorem Th28: :: WAYBEL13:28

for L1, L2 being non empty up-complete Poset

for f being Function of L1,L2 st f is isomorphic holds

for x being Element of L1 holds

( x is compact iff f . x is compact )

for f being Function of L1,L2 st f is isomorphic holds

for x being Element of L1 holds

( x is compact iff f . x is compact )

proof end;

theorem Th29: :: WAYBEL13:29

for L1, L2 being non empty up-complete Poset

for f being Function of L1,L2 st f is isomorphic holds

for x being Element of L1 holds f .: (compactbelow x) = compactbelow (f . x)

for f being Function of L1,L2 st f is isomorphic holds

for x being Element of L1 holds f .: (compactbelow x) = compactbelow (f . x)

proof end;

theorem Th30: :: WAYBEL13:30

for L1, L2 being non empty Poset st L1,L2 are_isomorphic & L1 is up-complete holds

L2 is up-complete

L2 is up-complete

proof end;

theorem Th31: :: WAYBEL13:31

for L1, L2 being non empty Poset st L1,L2 are_isomorphic & L1 is complete & L1 is satisfying_axiom_K holds

L2 is satisfying_axiom_K

L2 is satisfying_axiom_K

proof end;

theorem Th32: :: WAYBEL13:32

for L1, L2 being sup-Semilattice st L1,L2 are_isomorphic & L1 is lower-bounded & L1 is algebraic holds

L2 is algebraic

L2 is algebraic

proof end;

Lm5: for L being LATTICE st ex X being set ex c being closure Function of (BoolePoset X),(BoolePoset X) st

( c is directed-sups-preserving & L, Image c are_isomorphic ) holds

L is algebraic

proof end;

theorem :: WAYBEL13:33

for L being lower-bounded continuous sup-Semilattice holds

( SupMap L is infs-preserving & SupMap L is sups-preserving ) by WAYBEL_1:12, WAYBEL_1:57, WAYBEL_5:3;

( SupMap L is infs-preserving & SupMap L is sups-preserving ) by WAYBEL_1:12, WAYBEL_1:57, WAYBEL_5:3;

:: THEOREM 4.15. (1) iff (2)

theorem :: WAYBEL13:34

for L being lower-bounded LATTICE holds

( ( L is algebraic implies ex X being non empty set ex S being full SubRelStr of BoolePoset X st

( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) ) & ( ex X being set ex S being full SubRelStr of BoolePoset X st

( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) implies L is algebraic ) )

( ( L is algebraic implies ex X being non empty set ex S being full SubRelStr of BoolePoset X st

( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) ) & ( ex X being set ex S being full SubRelStr of BoolePoset X st

( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) implies L is algebraic ) )

proof end;

:: THEOREM 4.15. (1) iff (3)

theorem :: WAYBEL13:35

for L being lower-bounded LATTICE holds

( ( L is algebraic implies ex X being non empty set ex c being closure Function of (BoolePoset X),(BoolePoset X) st

( c is directed-sups-preserving & L, Image c are_isomorphic ) ) & ( ex X being set ex c being closure Function of (BoolePoset X),(BoolePoset X) st

( c is directed-sups-preserving & L, Image c are_isomorphic ) implies L is algebraic ) )

( ( L is algebraic implies ex X being non empty set ex c being closure Function of (BoolePoset X),(BoolePoset X) st

( c is directed-sups-preserving & L, Image c are_isomorphic ) ) & ( ex X being set ex c being closure Function of (BoolePoset X),(BoolePoset X) st

( c is directed-sups-preserving & L, Image c are_isomorphic ) implies L is algebraic ) )

proof end;