:: by Robert Milewski

::

:: Received October 29, 1997

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

theorem Th1: :: WAYBEL15:1

for R being RelStr

for S being full SubRelStr of R

for T being full SubRelStr of S holds T is full SubRelStr of R

for S being full SubRelStr of R

for T being full SubRelStr of S holds T is full SubRelStr of R

proof end;

Lm1: for X being set

for Y, Z being non empty set

for f being Function of X,Y

for g being Function of Y,Z st f is onto & g is onto holds

g * f is onto

by FUNCT_2:27;

theorem :: WAYBEL15:2

for X being set

for a being Element of (BoolePoset X) holds uparrow a = { Y where Y is Subset of X : a c= Y }

for a being Element of (BoolePoset X) holds uparrow a = { Y where Y is Subset of X : a c= Y }

proof end;

theorem :: WAYBEL15:3

for L being non empty antisymmetric upper-bounded RelStr

for a being Element of L st Top L <= a holds

a = Top L

for a being Element of L st Top L <= a holds

a = Top L

proof end;

theorem Th4: :: WAYBEL15:4

for S, T being non empty Poset

for g being Function of S,T

for d being Function of T,S st g is onto & [g,d] is Galois holds

T, Image d are_isomorphic

for g being Function of S,T

for d being Function of T,S st g is onto & [g,d] is Galois holds

T, Image d are_isomorphic

proof end;

theorem Th5: :: WAYBEL15:5

for L1, L2, L3 being non empty Poset

for g1 being Function of L1,L2

for g2 being Function of L2,L3

for d1 being Function of L2,L1

for d2 being Function of L3,L2 st [g1,d1] is Galois & [g2,d2] is Galois holds

[(g2 * g1),(d1 * d2)] is Galois

for g1 being Function of L1,L2

for g2 being Function of L2,L3

for d1 being Function of L2,L1

for d2 being Function of L3,L2 st [g1,d1] is Galois & [g2,d2] is Galois holds

[(g2 * g1),(d1 * d2)] is Galois

proof end;

theorem Th6: :: WAYBEL15:6

for L1, L2 being non empty Poset

for f being Function of L1,L2

for f1 being Function of L2,L1 st f1 = f " & f is isomorphic holds

( [f,f1] is Galois & [f1,f] is Galois )

for f being Function of L1,L2

for f1 being Function of L2,L1 st f1 = f " & f is isomorphic holds

( [f,f1] is Galois & [f1,f] is Galois )

proof end;

registration
end;

theorem Th8: :: WAYBEL15:8

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 .: (waybelow x) = waybelow (f . x)

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

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

proof end;

theorem Th10: :: WAYBEL15:10

for L1, L2 being LATTICE st L1,L2 are_isomorphic & L1 is lower-bounded & L1 is arithmetic holds

L2 is arithmetic

L2 is arithmetic

proof end;

Lm2: for L being lower-bounded LATTICE st L is continuous holds

ex A being lower-bounded arithmetic LATTICE ex g being Function of A,L st

( g is onto & g is infs-preserving & g is directed-sups-preserving )

proof end;

theorem Th11: :: WAYBEL15:11

for L1, L2, L3 being non empty Poset

for f being Function of L1,L2

for g being Function of L2,L3 st f is directed-sups-preserving & g is directed-sups-preserving holds

g * f is directed-sups-preserving

for f being Function of L1,L2

for g being Function of L2,L3 st f is directed-sups-preserving & g is directed-sups-preserving holds

g * f is directed-sups-preserving

proof end;

theorem :: WAYBEL15:12

theorem Th13: :: WAYBEL15:13

for X being set

for c being Function of (BoolePoset X),(BoolePoset X) st c is idempotent & c is directed-sups-preserving holds

inclusion c is directed-sups-preserving

for c being Function of (BoolePoset X),(BoolePoset X) st c is idempotent & c is directed-sups-preserving holds

inclusion c is directed-sups-preserving

proof end;

Lm3: for L being lower-bounded LATTICE st ex A being lower-bounded algebraic LATTICE ex g being Function of A,L st

( g is onto & g is infs-preserving & g is directed-sups-preserving ) holds

ex X being non empty set ex p being projection Function of (BoolePoset X),(BoolePoset X) st

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

proof end;

theorem Th14: :: WAYBEL15:14

for L being complete continuous LATTICE

for p being kernel Function of L,L st p is directed-sups-preserving holds

Image p is continuous LATTICE

for p being kernel Function of L,L st p is directed-sups-preserving holds

Image p is continuous LATTICE

proof end;

theorem Th15: :: WAYBEL15:15

for L being complete continuous LATTICE

for p being projection Function of L,L st p is directed-sups-preserving holds

Image p is continuous LATTICE

for p being projection Function of L,L st p is directed-sups-preserving holds

Image p is continuous LATTICE

proof end;

Lm4: for L being LATTICE st ex X being set ex p being projection Function of (BoolePoset X),(BoolePoset X) st

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

L is continuous

proof end;

theorem :: WAYBEL15:16

for L being lower-bounded LATTICE holds

( L is continuous iff ex A being lower-bounded arithmetic LATTICE ex g being Function of A,L st

( g is onto & g is infs-preserving & g is directed-sups-preserving ) )

( L is continuous iff ex A being lower-bounded arithmetic LATTICE ex g being Function of A,L st

( g is onto & g is infs-preserving & g is directed-sups-preserving ) )

proof end;

theorem :: WAYBEL15:17

for L being lower-bounded LATTICE holds

( L is continuous iff ex A being lower-bounded algebraic LATTICE ex g being Function of A,L st

( g is onto & g is infs-preserving & g is directed-sups-preserving ) )

( L is continuous iff ex A being lower-bounded algebraic LATTICE ex g being Function of A,L st

( g is onto & g is infs-preserving & g is directed-sups-preserving ) )

proof end;

theorem :: WAYBEL15:18

for L being lower-bounded LATTICE holds

( ( L is continuous implies ex X being non empty set ex p being projection Function of (BoolePoset X),(BoolePoset X) st

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

( p is directed-sups-preserving & L, Image p are_isomorphic ) implies L is continuous ) )

( ( L is continuous implies ex X being non empty set ex p being projection Function of (BoolePoset X),(BoolePoset X) st

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

( p is directed-sups-preserving & L, Image p are_isomorphic ) implies L is continuous ) )

proof end;

theorem :: WAYBEL15:19

for L being non empty RelStr

for x being Element of L holds

( x in PRIME (L opp) iff x is co-prime )

for x being Element of L holds

( x in PRIME (L opp) iff x is co-prime )

proof end;

:: deftheorem defines atom WAYBEL15:def 1 :

for L being non empty RelStr

for a being Element of L holds

( a is atom iff ( Bottom L < a & ( for b being Element of L st Bottom L < b & b <= a holds

b = a ) ) );

for L being non empty RelStr

for a being Element of L holds

( a is atom iff ( Bottom L < a & ( for b being Element of L st Bottom L < b & b <= a holds

b = a ) ) );

definition

let L be non empty RelStr ;

ex b_{1} being Subset of L st

for x being Element of L holds

( x in b_{1} iff x is atom )

for b_{1}, b_{2} being Subset of L st ( for x being Element of L holds

( x in b_{1} iff x is atom ) ) & ( for x being Element of L holds

( x in b_{2} iff x is atom ) ) holds

b_{1} = b_{2}

end;
func ATOM L -> Subset of L means :Def2: :: WAYBEL15:def 2

for x being Element of L holds

( x in it iff x is atom );

existence for x being Element of L holds

( x in it iff x is atom );

ex b

for x being Element of L holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def2 defines ATOM WAYBEL15:def 2 :

for L being non empty RelStr

for b_{2} being Subset of L holds

( b_{2} = ATOM L iff for x being Element of L holds

( x in b_{2} iff x is atom ) );

for L being non empty RelStr

for b

( b

( x in b

theorem Th20: :: WAYBEL15:20

for L being Boolean LATTICE

for a being Element of L holds

( a is atom iff ( a is co-prime & a <> Bottom L ) )

for a being Element of L holds

( a is atom iff ( a is co-prime & a <> Bottom L ) )

proof end;

registration

let L be Boolean LATTICE;

coherence

for b_{1} being Element of L st b_{1} is atom holds

b_{1} is co-prime
by Th20;

end;
coherence

for b

b

theorem :: WAYBEL15:22

for L being Boolean LATTICE

for x, a being Element of L st a is atom holds

( a <= x iff not a <= 'not' x )

for x, a being Element of L st a is atom holds

( a <= x iff not a <= 'not' x )

proof end;

theorem Th23: :: WAYBEL15:23

for L being complete Boolean LATTICE

for X being Subset of L

for x being Element of L holds x "/\" (sup X) = "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L)

for X being Subset of L

for x being Element of L holds x "/\" (sup X) = "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L)

proof end;

theorem Th24: :: WAYBEL15:24

for L being non empty antisymmetric with_infima lower-bounded RelStr

for x, y being Element of L st x is atom & y is atom & x <> y holds

x "/\" y = Bottom L

for x, y being Element of L st x is atom & y is atom & x <> y holds

x "/\" y = Bottom L

proof end;

theorem Th25: :: WAYBEL15:25

for L being complete Boolean LATTICE

for x being Element of L

for A being Subset of L st A c= ATOM L holds

( x in A iff ( x is atom & x <= sup A ) )

for x being Element of L

for A being Subset of L st A c= ATOM L holds

( x in A iff ( x is atom & x <= sup A ) )

proof end;

theorem Th26: :: WAYBEL15:26

for L being complete Boolean LATTICE

for X, Y being Subset of L st X c= ATOM L & Y c= ATOM L holds

( X c= Y iff sup X <= sup Y )

for X, Y being Subset of L st X c= ATOM L & Y c= ATOM L holds

( X c= Y iff sup X <= sup Y )

proof end;

Lm5: for L being Boolean LATTICE st L is completely-distributive holds

( L is complete & ( for x being Element of L ex X being Subset of L st

( X c= ATOM L & x = sup X ) ) )

proof end;

Lm6: for L being Boolean LATTICE st L is complete & ( for x being Element of L ex X being Subset of L st

( X c= ATOM L & x = sup X ) ) holds

ex Y being set st L, BoolePoset Y are_isomorphic

proof end;

theorem :: WAYBEL15:27

for L being Boolean LATTICE holds

( L is arithmetic iff ex X being set st L, BoolePoset X are_isomorphic )

( L is arithmetic iff ex X being set st L, BoolePoset X are_isomorphic )

proof end;

theorem :: WAYBEL15:32

for L being Boolean LATTICE holds

( L is arithmetic iff ( L is complete & ( for x being Element of L ex X being Subset of L st

( X c= ATOM L & x = sup X ) ) ) )

( L is arithmetic iff ( L is complete & ( for x being Element of L ex X being Subset of L st

( X c= ATOM L & x = sup X ) ) ) )

proof end;