:: by Beata Madras

::

:: Received December 1, 1996

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

begin

:: Preliminaries

scheme :: WAYBEL_6:sch 1

NonUniqExD1{ F_{1}() -> non empty RelStr , F_{2}() -> Subset of F_{1}(), F_{3}() -> non empty Subset of F_{1}(), P_{1}[ set , set ] } :

NonUniqExD1{ F

ex f being Function of F_{2}(),F_{3}() st

for e being Element of F_{1}() st e in F_{2}() holds

ex u being Element of F_{1}() st

( u in F_{3}() & u = f . e & P_{1}[e,u] )

providedfor e being Element of F

ex u being Element of F

( u in F

A1:
for e being Element of F_{1}() st e in F_{2}() holds

ex u being Element of F_{1}() st

( u in F_{3}() & P_{1}[e,u] )

ex u being Element of F

( u in F

proof end;

definition

let L be LATTICE;

let A be non empty Subset of L;

let f be Function of A,A;

let n be Element of NAT ;

:: original: iter

redefine func iter (f,n) -> Function of A,A;

coherence

iter (f,n) is Function of A,A by FUNCT_7:83;

end;
let A be non empty Subset of L;

let f be Function of A,A;

let n be Element of NAT ;

:: original: iter

redefine func iter (f,n) -> Function of A,A;

coherence

iter (f,n) is Function of A,A by FUNCT_7:83;

definition

let L be LATTICE;

let C, D be non empty Subset of L;

let f be Function of C,D;

let c be Element of C;

:: original: .

redefine func f . c -> Element of L;

coherence

f . c is Element of L

end;
let C, D be non empty Subset of L;

let f be Function of C,D;

let c be Element of C;

:: original: .

redefine func f . c -> Element of L;

coherence

f . c is Element of L

proof end;

registration

let L be non empty Poset;

coherence

for b_{1} being Chain of L holds

( b_{1} is filtered & b_{1} is directed )

end;
coherence

for b

( b

proof end;

registration

ex b_{1} being LATTICE st

( b_{1} is strict & b_{1} is continuous & b_{1} is distributive & b_{1} is lower-bounded )
end;

cluster non empty strict V110() reflexive transitive antisymmetric lower-bounded distributive with_suprema with_infima continuous for RelStr ;

existence ex b

( b

proof end;

theorem Th1: :: WAYBEL_6:1

for S, T being Semilattice

for f being Function of S,T holds

( f is meet-preserving iff for x, y being Element of S holds f . (x "/\" y) = (f . x) "/\" (f . y) )

for f being Function of S,T holds

( f is meet-preserving iff for x, y being Element of S holds f . (x "/\" y) = (f . x) "/\" (f . y) )

proof end;

theorem Th2: :: WAYBEL_6:2

for S, T being sup-Semilattice

for f being Function of S,T holds

( f is join-preserving iff for x, y being Element of S holds f . (x "\/" y) = (f . x) "\/" (f . y) )

for f being Function of S,T holds

( f is join-preserving iff for x, y being Element of S holds f . (x "\/" y) = (f . x) "\/" (f . y) )

proof end;

theorem Th3: :: WAYBEL_6:3

for S, T being LATTICE

for f being Function of S,T st T is distributive & f is meet-preserving & f is join-preserving & f is V24() holds

S is distributive

for f being Function of S,T st T is distributive & f is meet-preserving & f is join-preserving & f is V24() holds

S is distributive

proof end;

registration

let S, T be complete LATTICE;

ex b_{1} being Function of S,T st b_{1} is sups-preserving

end;
cluster Relation-like the carrier of S -defined the carrier of T -valued Function-like V32( the carrier of S, the carrier of T) sups-preserving for Element of bool [: the carrier of S, the carrier of T:];

existence ex b

proof end;

Lm1: for S, T being non empty with_suprema Poset

for f being Function of S,T st f is directed-sups-preserving holds

f is monotone

proof end;

theorem Th4: :: WAYBEL_6:4

for S, T being complete LATTICE

for f being sups-preserving Function of S,T st T is meet-continuous & f is meet-preserving & f is V24() holds

S is meet-continuous

for f being sups-preserving Function of S,T st T is meet-continuous & f is meet-preserving & f is V24() holds

S is meet-continuous

proof end;

begin

:: deftheorem Def1 defines Open WAYBEL_6:def 1 :

for L being non empty reflexive RelStr

for X being Subset of L holds

( X is Open iff for x being Element of L st x in X holds

ex y being Element of L st

( y in X & y << x ) );

for L being non empty reflexive RelStr

for X being Subset of L holds

( X is Open iff for x being Element of L st x in X holds

ex y being Element of L st

( y in X & y << x ) );

theorem :: WAYBEL_6:5

for L being up-complete LATTICE

for X being upper Subset of L holds

( X is Open iff for x being Element of L st x in X holds

waybelow x meets X )

for X being upper Subset of L holds

( X is Open iff for x being Element of L st x in X holds

waybelow x meets X )

proof end;

theorem :: WAYBEL_6:6

for L being up-complete LATTICE

for X being upper Subset of L holds

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

for X being upper Subset of L holds

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

proof end;

registration

let L be lower-bounded up-complete LATTICE;

existence

ex b_{1} being Filter of L st b_{1} is Open

end;
existence

ex b

proof end;

theorem Th8: :: WAYBEL_6:8

for L being lower-bounded continuous LATTICE

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

ex F being Open Filter of L st

( y in F & F c= wayabove x )

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

ex F being Open Filter of L st

( y in F & F c= wayabove x )

proof end;

theorem Th9: :: WAYBEL_6:9

for L being complete LATTICE

for X being upper Open Subset of L

for x being Element of L st x in X ` holds

ex m being Element of L st

( x <= m & m is_maximal_in X ` )

for X being upper Open Subset of L

for x being Element of L st x in X ` holds

ex m being Element of L st

( x <= m & m is_maximal_in X ` )

proof end;

begin

definition

let G be non empty RelStr ;

let g be Element of G;

end;
let g be Element of G;

attr g is meet-irreducible means :Def2: :: WAYBEL_6:def 2

for x, y being Element of G holds

( not g = x "/\" y or x = g or y = g );

for x, y being Element of G holds

( not g = x "/\" y or x = g or y = g );

:: deftheorem Def2 defines meet-irreducible WAYBEL_6:def 2 :

for G being non empty RelStr

for g being Element of G holds

( g is meet-irreducible iff for x, y being Element of G holds

( not g = x "/\" y or x = g or y = g ) );

for G being non empty RelStr

for g being Element of G holds

( g is meet-irreducible iff for x, y being Element of G holds

( not g = x "/\" y or x = g or y = g ) );

notation
end;

definition

let G be non empty RelStr ;

let g be Element of G;

end;
let g be Element of G;

attr g is join-irreducible means :: WAYBEL_6:def 3

for x, y being Element of G holds

( not g = x "\/" y or x = g or y = g );

for x, y being Element of G holds

( not g = x "\/" y or x = g or y = g );

:: deftheorem defines join-irreducible WAYBEL_6:def 3 :

for G being non empty RelStr

for g being Element of G holds

( g is join-irreducible iff for x, y being Element of G holds

( not g = x "\/" y or x = g or y = g ) );

for G being non empty RelStr

for g being Element of G holds

( g is join-irreducible iff for x, y being Element of G holds

( not g = x "\/" y or x = g or y = g ) );

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 irreducible )

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

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

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

b_{1} = b_{2}

end;
func IRR L -> Subset of L means :Def4: :: WAYBEL_6:def 4

for x being Element of L holds

( x in it iff x is irreducible );

existence for x being Element of L holds

( x in it iff x is irreducible );

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 Def4 defines IRR WAYBEL_6:def 4 :

for L being non empty RelStr

for b_{2} being Subset of L holds

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

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

for L being non empty RelStr

for b

( b

( x in b

registration

let L be non empty antisymmetric upper-bounded with_infima RelStr ;

existence

ex b_{1} being Element of L st b_{1} is irreducible

end;
existence

ex b

proof end;

theorem :: WAYBEL_6:11

for L being Semilattice

for x being Element of L holds

( x is irreducible iff for A being non empty finite Subset of L st x = inf A holds

x in A )

for x being Element of L holds

( x is irreducible iff for A being non empty finite Subset of L st x = inf A holds

x in A )

proof end;

theorem :: WAYBEL_6:12

for L being LATTICE

for l being Element of L st (uparrow l) \ {l} is Filter of L holds

l is irreducible

for l being Element of L st (uparrow l) \ {l} is Filter of L holds

l is irreducible

proof end;

theorem Th13: :: WAYBEL_6:13

for L being LATTICE

for p being Element of L

for F being Filter of L st p is_maximal_in F ` holds

p is irreducible

for p being Element of L

for F being Filter of L st p is_maximal_in F ` holds

p is irreducible

proof end;

theorem Th14: :: WAYBEL_6:14

for L being lower-bounded continuous LATTICE

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

ex p being Element of L st

( p is irreducible & x <= p & not y <= p )

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

ex p being Element of L st

( p is irreducible & x <= p & not y <= p )

proof end;

begin

:: deftheorem Def5 defines order-generating WAYBEL_6:def 5 :

for L being non empty RelStr

for X being Subset of L holds

( X is order-generating iff for x being Element of L holds

( ex_inf_of (uparrow x) /\ X,L & x = inf ((uparrow x) /\ X) ) );

for L being non empty RelStr

for X being Subset of L holds

( X is order-generating iff for x being Element of L holds

( ex_inf_of (uparrow x) /\ X,L & x = inf ((uparrow x) /\ X) ) );

theorem Th15: :: WAYBEL_6:15

for L being lower-bounded up-complete LATTICE

for X being Subset of L holds

( X is order-generating iff for l being Element of L ex Y being Subset of X st l = "/\" (Y,L) )

for X being Subset of L holds

( X is order-generating iff for l being Element of L ex Y being Subset of X st l = "/\" (Y,L) )

proof end;

theorem :: WAYBEL_6:16

for L being lower-bounded up-complete LATTICE

for X being Subset of L holds

( X is order-generating iff for Y being Subset of L st X c= Y & ( for Z being Subset of Y holds "/\" (Z,L) in Y ) holds

the carrier of L = Y )

for X being Subset of L holds

( X is order-generating iff for Y being Subset of L st X c= Y & ( for Z being Subset of Y holds "/\" (Z,L) in Y ) holds

the carrier of L = Y )

proof end;

theorem Th17: :: WAYBEL_6:17

for L being lower-bounded up-complete LATTICE

for X being Subset of L holds

( X is order-generating iff for l1, l2 being Element of L st not l2 <= l1 holds

ex p being Element of L st

( p in X & l1 <= p & not l2 <= p ) )

for X being Subset of L holds

( X is order-generating iff for l1, l2 being Element of L st not l2 <= l1 holds

ex p being Element of L st

( p in X & l1 <= p & not l2 <= p ) )

proof end;

theorem Th18: :: WAYBEL_6:18

for L being lower-bounded continuous LATTICE

for X being Subset of L st X = (IRR L) \ {(Top L)} holds

X is order-generating

for X being Subset of L st X = (IRR L) \ {(Top L)} holds

X is order-generating

proof end;

theorem Th19: :: WAYBEL_6:19

for L being lower-bounded continuous LATTICE

for X, Y being Subset of L st X is order-generating & X c= Y holds

Y is order-generating

for X, Y being Subset of L st X is order-generating & X c= Y holds

Y is order-generating

proof end;

begin

:: deftheorem Def6 defines prime WAYBEL_6:def 6 :

for L being non empty RelStr

for l being Element of L holds

( l is prime iff for x, y being Element of L holds

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

for L being non empty RelStr

for l being Element of L holds

( l is prime iff for x, y being Element of L holds

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

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 prime )

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

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

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

b_{1} = b_{2}

end;
func PRIME L -> Subset of L means :Def7: :: WAYBEL_6:def 7

for x being Element of L holds

( x in it iff x is prime );

existence for x being Element of L holds

( x in it iff x is prime );

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 Def7 defines PRIME WAYBEL_6:def 7 :

for L being non empty RelStr

for b_{2} being Subset of L holds

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

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

for L being non empty RelStr

for b

( b

( x in b

:: deftheorem Def8 defines co-prime WAYBEL_6:def 8 :

for L being non empty RelStr

for l being Element of L holds

( l is co-prime iff l ~ is prime );

for L being non empty RelStr

for l being Element of L holds

( l is co-prime iff l ~ is prime );

registration

let L be non empty antisymmetric upper-bounded RelStr ;

existence

ex b_{1} being Element of L st b_{1} is prime

end;
existence

ex b

proof end;

theorem Th22: :: WAYBEL_6:22

for L being Semilattice

for l being Element of L holds

( l is prime iff for A being non empty finite Subset of L st l >= inf A holds

ex a being Element of L st

( a in A & l >= a ) )

for l being Element of L holds

( l is prime iff for A being non empty finite Subset of L st l >= inf A holds

ex a being Element of L st

( a in A & l >= a ) )

proof end;

theorem Th23: :: WAYBEL_6:23

for L being sup-Semilattice

for x being Element of L holds

( x is co-prime iff for A being non empty finite Subset of L st x <= sup A holds

ex a being Element of L st

( a in A & x <= a ) )

for x being Element of L holds

( x is co-prime iff for A being non empty finite Subset of L st x <= sup A holds

ex a being Element of L st

( a in A & x <= a ) )

proof end;

theorem Th25: :: WAYBEL_6:25

for L being LATTICE

for l being Element of L holds

( l is prime iff for x being set

for f being Function of L,(BoolePoset {x}) st ( for p being Element of L holds

( f . p = {} iff p <= l ) ) holds

( f is meet-preserving & f is join-preserving ) )

for l being Element of L holds

( l is prime iff for x being set

for f being Function of L,(BoolePoset {x}) st ( for p being Element of L holds

( f . p = {} iff p <= l ) ) holds

( f is meet-preserving & f is join-preserving ) )

proof end;

theorem Th26: :: WAYBEL_6:26

for L being upper-bounded LATTICE

for l being Element of L st l <> Top L holds

( l is prime iff (downarrow l) ` is Filter of L )

for l being Element of L st l <> Top L holds

( l is prime iff (downarrow l) ` is Filter of L )

proof end;

theorem :: WAYBEL_6:29

for L being Boolean LATTICE

for l being Element of L st l <> Top L holds

( l is prime iff for x being Element of L st x > l holds

x = Top L )

for l being Element of L st l <> Top L holds

( l is prime iff for x being Element of L st x > l holds

x = Top L )

proof end;

theorem :: WAYBEL_6:30

for L being lower-bounded distributive continuous LATTICE

for l being Element of L st l <> Top L holds

( l is prime iff ex F being Open Filter of L st l is_maximal_in F ` )

for l being Element of L st l <> Top L holds

( l is prime iff ex F being Open Filter of L st l is_maximal_in F ` )

proof end;

theorem Th31: :: WAYBEL_6:31

for L being RelStr

for X being Subset of L holds chi (X, the carrier of L) is Function of L,(BoolePoset {{}})

for X being Subset of L holds chi (X, the carrier of L) is Function of L,(BoolePoset {{}})

proof end;

theorem Th32: :: WAYBEL_6:32

for L being non empty RelStr

for p, x being Element of L holds

( (chi (((downarrow p) `), the carrier of L)) . x = {} iff x <= p )

for p, x being Element of L holds

( (chi (((downarrow p) `), the carrier of L)) . x = {} iff x <= p )

proof end;

theorem Th33: :: WAYBEL_6:33

for L being upper-bounded LATTICE

for f being Function of L,(BoolePoset {{}})

for p being prime Element of L st chi (((downarrow p) `), the carrier of L) = f holds

( f is meet-preserving & f is join-preserving )

for f being Function of L,(BoolePoset {{}})

for p being prime Element of L st chi (((downarrow p) `), the carrier of L) = f holds

( f is meet-preserving & f is join-preserving )

proof end;

theorem Th34: :: WAYBEL_6:34

for L being complete LATTICE st PRIME L is order-generating holds

( L is distributive & L is meet-continuous )

( L is distributive & L is meet-continuous )

proof end;

theorem Th35: :: WAYBEL_6:35

for L being lower-bounded continuous LATTICE holds

( L is distributive iff PRIME L is order-generating )

( L is distributive iff PRIME L is order-generating )

proof end;

theorem Th37: :: WAYBEL_6:37

for L being complete continuous LATTICE st ( for l being Element of L ex X being Subset of L st

( l = sup X & ( for x being Element of L st x in X holds

x is co-prime ) ) ) holds

for l being Element of L holds l = "\/" (((waybelow l) /\ (PRIME (L opp))),L)

( l = sup X & ( for x being Element of L st x in X holds

x is co-prime ) ) ) holds

for l being Element of L holds l = "\/" (((waybelow l) /\ (PRIME (L opp))),L)

proof end;

Lm2: for L being complete continuous LATTICE st ( for l being Element of L ex X being Subset of L st

( l = sup X & ( for x being Element of L st x in X holds

x is co-prime ) ) ) holds

L is completely-distributive

proof end;

Lm3: for L being complete completely-distributive LATTICE holds

( L is distributive & L is continuous & L ~ is continuous )

proof end;

Lm4: for L being complete LATTICE st L is distributive & L is continuous & L ~ is continuous holds

for l being Element of L ex X being Subset of L st

( l = sup X & ( for x being Element of L st x in X holds

x is co-prime ) )

proof end;

theorem :: WAYBEL_6:38

for L being complete LATTICE holds

( L is completely-distributive iff ( L is continuous & ( for l being Element of L ex X being Subset of L st

( l = sup X & ( for x being Element of L st x in X holds

x is co-prime ) ) ) ) )

( L is completely-distributive iff ( L is continuous & ( for l being Element of L ex X being Subset of L st

( l = sup X & ( for x being Element of L st x in X holds

x is co-prime ) ) ) ) )

proof end;

theorem :: WAYBEL_6:39

for L being complete LATTICE holds

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

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

proof end;