:: by Andrzej Trybulec

::

:: Received August 10, 1990

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

begin

theorem Th1: :: LATTICE2:1

for A being set

for C being non empty set

for B being Subset of A

for g being Function of A,C holds dom (g | B) = B

for C being non empty set

for B being Subset of A

for g being Function of A,C holds dom (g | B) = B

proof end;

theorem Th2: :: LATTICE2:2

for A being set

for C being non empty set

for B being Subset of A

for f, g being Function of A,C holds

( f | B = g | B iff for x being Element of A st x in B holds

g . x = f . x )

for C being non empty set

for B being Subset of A

for f, g being Function of A,C holds

( f | B = g | B iff for x being Element of A st x in B holds

g . x = f . x )

proof end;

theorem Th3: :: LATTICE2:3

for A being set

for C being non empty set

for f, g being Function of A,C

for B being set holds f +* (g | B) is Function of A,C

for C being non empty set

for f, g being Function of A,C

for B being set holds f +* (g | B) is Function of A,C

proof end;

theorem Th4: :: LATTICE2:4

for A being set

for C being non empty set

for B being Subset of A

for g, f being Function of A,C holds (g | B) +* f = f

for C being non empty set

for B being Subset of A

for g, f being Function of A,C holds (g | B) +* f = f

proof end;

theorem :: LATTICE2:6

theorem Th7: :: LATTICE2:7

for A being set

for C being non empty set

for B being Subset of A

for g, f being Function of A,C st ( for x being Element of A st x in B holds

g . x = f . x ) holds

f +* (g | B) = f

for C being non empty set

for B being Subset of A

for g, f being Function of A,C st ( for x being Element of A st x in B holds

g . x = f . x ) holds

f +* (g | B) = f

proof end;

theorem :: LATTICE2:8

for A being set

for C being non empty set

for g, f being Function of A,C

for B being Finite_Subset of A holds (g | B) +* f = f

for C being non empty set

for g, f being Function of A,C

for B being Finite_Subset of A holds (g | B) +* f = f

proof end;

theorem Th9: :: LATTICE2:9

for A being set

for C being non empty set

for g being Function of A,C

for B being Finite_Subset of A holds dom (g | B) = B

for C being non empty set

for g being Function of A,C

for B being Finite_Subset of A holds dom (g | B) = B

proof end;

theorem Th10: :: LATTICE2:10

for A being set

for C being non empty set

for g, f being Function of A,C

for B being Finite_Subset of A st ( for x being Element of A st x in B holds

g . x = f . x ) holds

f +* (g | B) = f

for C being non empty set

for g, f being Function of A,C

for B being Finite_Subset of A st ( for x being Element of A st x in B holds

g . x = f . x ) holds

f +* (g | B) = f

proof end;

:: deftheorem Def1 defines absorbs LATTICE2:def 1 :

for D being non empty set

for o, o9 being BinOp of D holds

( o absorbs o9 iff for x, y being Element of D holds o . (x,(o9 . (x,y))) = x );

for D being non empty set

for o, o9 being BinOp of D holds

( o absorbs o9 iff for x, y being Element of D holds o . (x,(o9 . (x,y))) = x );

notation
end;

theorem Th11: :: LATTICE2:11

for L being non empty LattStr st the L_join of L is commutative & the L_join of L is associative & the L_meet of L is commutative & the L_meet of L is associative & the L_join of L absorbs the L_meet of L & the L_meet of L absorbs the L_join of L holds

L is Lattice-like

L is Lattice-like

proof end;

definition

let L be LattStr ;

coherence

LattStr(# the carrier of L, the L_meet of L, the L_join of L #) is strict LattStr ;

;

end;
func L .: -> strict LattStr equals :: LATTICE2:def 2

LattStr(# the carrier of L, the L_meet of L, the L_join of L #);

correctness LattStr(# the carrier of L, the L_meet of L, the L_join of L #);

coherence

LattStr(# the carrier of L, the L_meet of L, the L_join of L #) is strict LattStr ;

;

:: deftheorem defines .: LATTICE2:def 2 :

for L being LattStr holds L .: = LattStr(# the carrier of L, the L_meet of L, the L_join of L #);

for L being LattStr holds L .: = LattStr(# the carrier of L, the L_meet of L, the L_join of L #);

registration
end;

theorem :: LATTICE2:12

theorem Th14: :: LATTICE2:14

for L being Lattice

for u being Element of L st ( for v being Element of L holds u "\/" v = v ) holds

u = Bottom L

for u being Element of L st ( for v being Element of L holds u "\/" v = v ) holds

u = Bottom L

proof end;

theorem Th15: :: LATTICE2:15

for L being Lattice

for u being Element of L st ( for v being Element of L holds the L_join of L . (u,v) = v ) holds

u = Bottom L

for u being Element of L st ( for v being Element of L holds the L_join of L . (u,v) = v ) holds

u = Bottom L

proof end;

theorem Th16: :: LATTICE2:16

for L being Lattice

for u being Element of L st ( for v being Element of L holds u "/\" v = v ) holds

u = Top L

for u being Element of L st ( for v being Element of L holds u "/\" v = v ) holds

u = Top L

proof end;

theorem Th17: :: LATTICE2:17

for L being Lattice

for u being Element of L st ( for v being Element of L holds the L_meet of L . (u,v) = v ) holds

u = Top L

for u being Element of L st ( for v being Element of L holds the L_meet of L . (u,v) = v ) holds

u = Top L

proof end;

registration

let L be non empty join-commutative \/-SemiLattStr ;

coherence

the L_join of L is commutative

end;
coherence

the L_join of L is commutative

proof end;

theorem Th18: :: LATTICE2:18

for L being Lattice st the L_join of L is having_a_unity holds

Bottom L = the_unity_wrt the L_join of L

Bottom L = the_unity_wrt the L_join of L

proof end;

registration

let L be non empty join-associative \/-SemiLattStr ;

coherence

the L_join of L is associative

end;
coherence

the L_join of L is associative

proof end;

registration

let L be non empty meet-commutative /\-SemiLattStr ;

coherence

the L_meet of L is commutative

end;
coherence

the L_meet of L is commutative

proof end;

registration

let L be non empty meet-associative /\-SemiLattStr ;

coherence

the L_meet of L is associative

end;
coherence

the L_meet of L is associative

proof end;

theorem Th19: :: LATTICE2:19

for L being Lattice st the L_meet of L is having_a_unity holds

Top L = the_unity_wrt the L_meet of L

Top L = the_unity_wrt the L_meet of L

proof end;

definition

let A be non empty set ;

let L be Lattice;

let B be Finite_Subset of A;

let f be Function of A, the carrier of L;

correctness

coherence

the L_join of L $$ (B,f) is Element of L;

;

correctness

coherence

the L_meet of L $$ (B,f) is Element of L;

;

end;
let L be Lattice;

let B be Finite_Subset of A;

let f be Function of A, the carrier of L;

correctness

coherence

the L_join of L $$ (B,f) is Element of L;

;

correctness

coherence

the L_meet of L $$ (B,f) is Element of L;

;

:: deftheorem defines FinJoin LATTICE2:def 3 :

for A being non empty set

for L being Lattice

for B being Finite_Subset of A

for f being Function of A, the carrier of L holds FinJoin (B,f) = the L_join of L $$ (B,f);

for A being non empty set

for L being Lattice

for B being Finite_Subset of A

for f being Function of A, the carrier of L holds FinJoin (B,f) = the L_join of L $$ (B,f);

:: deftheorem defines FinMeet LATTICE2:def 4 :

for A being non empty set

for L being Lattice

for B being Finite_Subset of A

for f being Function of A, the carrier of L holds FinMeet (B,f) = the L_meet of L $$ (B,f);

for A being non empty set

for L being Lattice

for B being Finite_Subset of A

for f being Function of A, the carrier of L holds FinMeet (B,f) = the L_meet of L $$ (B,f);

theorem Th28: :: LATTICE2:28

for L being Lattice

for A being non empty set

for x being Element of A

for B being Finite_Subset of A

for f being Function of A, the carrier of L st x in B holds

f . x [= FinJoin (B,f)

for A being non empty set

for x being Element of A

for B being Finite_Subset of A

for f being Function of A, the carrier of L st x in B holds

f . x [= FinJoin (B,f)

proof end;

theorem Th29: :: LATTICE2:29

for L being Lattice

for u being Element of L

for A being non empty set

for B being Finite_Subset of A

for f being Function of A, the carrier of L st ex x being Element of A st

( x in B & u [= f . x ) holds

u [= FinJoin (B,f)

for u being Element of L

for A being non empty set

for B being Finite_Subset of A

for f being Function of A, the carrier of L st ex x being Element of A st

( x in B & u [= f . x ) holds

u [= FinJoin (B,f)

proof end;

theorem :: LATTICE2:30

theorem :: LATTICE2:31

for L being Lattice

for u being Element of L

for A being non empty set

for B being Finite_Subset of A

for f being Function of A, the carrier of L st FinJoin (B,f) [= u holds

for x being Element of A st x in B holds

f . x [= u

for u being Element of L

for A being non empty set

for B being Finite_Subset of A

for f being Function of A, the carrier of L st FinJoin (B,f) [= u holds

for x being Element of A st x in B holds

f . x [= u

proof end;

theorem Th32: :: LATTICE2:32

for L being Lattice

for u being Element of L

for A being non empty set

for B being Finite_Subset of A

for f being Function of A, the carrier of L st B <> {} & ( for x being Element of A st x in B holds

f . x [= u ) holds

FinJoin (B,f) [= u

for u being Element of L

for A being non empty set

for B being Finite_Subset of A

for f being Function of A, the carrier of L st B <> {} & ( for x being Element of A st x in B holds

f . x [= u ) holds

FinJoin (B,f) [= u

proof end;

theorem :: LATTICE2:33

for L being Lattice

for A being non empty set

for B being Finite_Subset of A

for f, g being Function of A, the carrier of L st B <> {} & ( for x being Element of A st x in B holds

f . x [= g . x ) holds

FinJoin (B,f) [= FinJoin (B,g)

for A being non empty set

for B being Finite_Subset of A

for f, g being Function of A, the carrier of L st B <> {} & ( for x being Element of A st x in B holds

f . x [= g . x ) holds

FinJoin (B,f) [= FinJoin (B,g)

proof end;

theorem Th34: :: LATTICE2:34

for L being Lattice

for A being non empty set

for B being Finite_Subset of A

for f, g being Function of A, the carrier of L st B <> {} & f | B = g | B holds

FinJoin (B,f) = FinJoin (B,g)

for A being non empty set

for B being Finite_Subset of A

for f, g being Function of A, the carrier of L st B <> {} & f | B = g | B holds

FinJoin (B,f) = FinJoin (B,g)

proof end;

theorem :: LATTICE2:35

registration
end;

theorem :: LATTICE2:36

theorem Th38: :: LATTICE2:38

for L being Lattice

for a, b being Element of L st a [= b holds

for a9, b9 being Element of (L .:) st a = a9 & b = b9 holds

b9 [= a9

for a, b being Element of L st a [= b holds

for a9, b9 being Element of (L .:) st a = a9 & b = b9 holds

b9 [= a9

proof end;

theorem Th39: :: LATTICE2:39

for L being Lattice

for a, b being Element of L

for a9, b9 being Element of (L .:) st a9 [= b9 & a = a9 & b = b9 holds

b [= a

for a, b being Element of L

for a9, b9 being Element of (L .:) st a9 [= b9 & a = a9 & b = b9 holds

b [= a

proof end;

:: Dualizations

theorem Th40: :: LATTICE2:40

for L being Lattice

for A being non empty set

for x being Element of A

for B being Finite_Subset of A

for f being Function of A, the carrier of L st x in B holds

FinMeet (B,f) [= f . x

for A being non empty set

for x being Element of A

for B being Finite_Subset of A

for f being Function of A, the carrier of L st x in B holds

FinMeet (B,f) [= f . x

proof end;

theorem Th41: :: LATTICE2:41

for L being Lattice

for u being Element of L

for A being non empty set

for B being Finite_Subset of A

for f being Function of A, the carrier of L st ex x being Element of A st

( x in B & f . x [= u ) holds

FinMeet (B,f) [= u

for u being Element of L

for A being non empty set

for B being Finite_Subset of A

for f being Function of A, the carrier of L st ex x being Element of A st

( x in B & f . x [= u ) holds

FinMeet (B,f) [= u

proof end;

theorem :: LATTICE2:42

theorem :: LATTICE2:43

theorem :: LATTICE2:44

for L being Lattice

for u being Element of L

for A being non empty set

for B being Finite_Subset of A

for f being Function of A, the carrier of L st u [= FinMeet (B,f) holds

for x being Element of A st x in B holds

u [= f . x

for u being Element of L

for A being non empty set

for B being Finite_Subset of A

for f being Function of A, the carrier of L st u [= FinMeet (B,f) holds

for x being Element of A st x in B holds

u [= f . x

proof end;

theorem :: LATTICE2:45

for L being Lattice

for A being non empty set

for B being Finite_Subset of A

for f, g being Function of A, the carrier of L st B <> {} & f | B = g | B holds

FinMeet (B,f) = FinMeet (B,g)

for A being non empty set

for B being Finite_Subset of A

for f, g being Function of A, the carrier of L st B <> {} & f | B = g | B holds

FinMeet (B,f) = FinMeet (B,g)

proof end;

theorem Th46: :: LATTICE2:46

for L being Lattice

for u being Element of L

for A being non empty set

for B being Finite_Subset of A

for f being Function of A, the carrier of L st B <> {} & ( for x being Element of A st x in B holds

u [= f . x ) holds

u [= FinMeet (B,f)

for u being Element of L

for A being non empty set

for B being Finite_Subset of A

for f being Function of A, the carrier of L st B <> {} & ( for x being Element of A st x in B holds

u [= f . x ) holds

u [= FinMeet (B,f)

proof end;

theorem :: LATTICE2:47

for L being Lattice

for A being non empty set

for B being Finite_Subset of A

for f, g being Function of A, the carrier of L st B <> {} & ( for x being Element of A st x in B holds

f . x [= g . x ) holds

FinMeet (B,f) [= FinMeet (B,g)

for A being non empty set

for B being Finite_Subset of A

for f, g being Function of A, the carrier of L st B <> {} & ( for x being Element of A st x in B holds

f . x [= g . x ) holds

FinMeet (B,f) [= FinMeet (B,g)

proof end;

theorem :: LATTICE2:50

theorem :: LATTICE2:52

theorem Th53: :: LATTICE2:53

for A being non empty set

for B being Finite_Subset of A

for L being 0_Lattice

for f, g being Function of A, the carrier of L st f | B = g | B holds

FinJoin (B,f) = FinJoin (B,g)

for B being Finite_Subset of A

for L being 0_Lattice

for f, g being Function of A, the carrier of L st f | B = g | B holds

FinJoin (B,f) = FinJoin (B,g)

proof end;

theorem Th54: :: LATTICE2:54

for A being non empty set

for B being Finite_Subset of A

for L being 0_Lattice

for f being Function of A, the carrier of L

for u being Element of L st ( for x being Element of A st x in B holds

f . x [= u ) holds

FinJoin (B,f) [= u

for B being Finite_Subset of A

for L being 0_Lattice

for f being Function of A, the carrier of L

for u being Element of L st ( for x being Element of A st x in B holds

f . x [= u ) holds

FinJoin (B,f) [= u

proof end;

theorem :: LATTICE2:55

for A being non empty set

for B being Finite_Subset of A

for L being 0_Lattice

for f, g being Function of A, the carrier of L st ( for x being Element of A st x in B holds

f . x [= g . x ) holds

FinJoin (B,f) [= FinJoin (B,g)

for B being Finite_Subset of A

for L being 0_Lattice

for f, g being Function of A, the carrier of L st ( for x being Element of A st x in B holds

f . x [= g . x ) holds

FinJoin (B,f) [= FinJoin (B,g)

proof end;

theorem :: LATTICE2:58

for A being non empty set

for B being Finite_Subset of A

for L being 1_Lattice

for f, g being Function of A, the carrier of L st f | B = g | B holds

FinMeet (B,f) = FinMeet (B,g)

for B being Finite_Subset of A

for L being 1_Lattice

for f, g being Function of A, the carrier of L st f | B = g | B holds

FinMeet (B,f) = FinMeet (B,g)

proof end;

theorem Th59: :: LATTICE2:59

for A being non empty set

for B being Finite_Subset of A

for L being 1_Lattice

for f being Function of A, the carrier of L

for u being Element of L st ( for x being Element of A st x in B holds

u [= f . x ) holds

u [= FinMeet (B,f)

for B being Finite_Subset of A

for L being 1_Lattice

for f being Function of A, the carrier of L

for u being Element of L st ( for x being Element of A st x in B holds

u [= f . x ) holds

u [= FinMeet (B,f)

proof end;

theorem :: LATTICE2:60

for A being non empty set

for B being Finite_Subset of A

for L being 1_Lattice

for f, g being Function of A, the carrier of L st ( for x being Element of A st x in B holds

f . x [= g . x ) holds

FinMeet (B,f) [= FinMeet (B,g)

for B being Finite_Subset of A

for L being 1_Lattice

for f, g being Function of A, the carrier of L st ( for x being Element of A st x in B holds

f . x [= g . x ) holds

FinMeet (B,f) [= FinMeet (B,g)

proof end;

::

:: Distributive lattices with the minimal element

::

:: Distributive lattices with the minimal element

::

theorem :: LATTICE2:63

theorem Th64: :: LATTICE2:64

for A being non empty set

for B being Finite_Subset of A

for L being D0_Lattice

for f being Function of A, the carrier of L

for u being Element of L holds the L_meet of L . (u,(FinJoin (B,f))) = FinJoin (B,( the L_meet of L [;] (u,f)))

for B being Finite_Subset of A

for L being D0_Lattice

for f being Function of A, the carrier of L

for u being Element of L holds the L_meet of L . (u,(FinJoin (B,f))) = FinJoin (B,( the L_meet of L [;] (u,f)))

proof end;

theorem :: LATTICE2:65

for A being non empty set

for B being Finite_Subset of A

for L being D0_Lattice

for g, f being Function of A, the carrier of L

for u being Element of L st ( for x being Element of A st x in B holds

g . x = u "/\" (f . x) ) holds

u "/\" (FinJoin (B,f)) = FinJoin (B,g)

for B being Finite_Subset of A

for L being D0_Lattice

for g, f being Function of A, the carrier of L

for u being Element of L st ( for x being Element of A st x in B holds

g . x = u "/\" (f . x) ) holds

u "/\" (FinJoin (B,f)) = FinJoin (B,g)

proof end;

theorem :: LATTICE2:66

:: Heyting Lattices

:: deftheorem Def5 defines Heyting LATTICE2:def 5 :

for IT being Lattice holds

( IT is Heyting iff ( IT is implicative & IT is lower-bounded ) );

for IT being Lattice holds

( IT is Heyting iff ( IT is implicative & IT is lower-bounded ) );

registration

ex b_{1} being Lattice st b_{1} is Heyting
end;

cluster non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like Heyting for LattStr ;

existence ex b

proof end;

registration

coherence

for b_{1} being Lattice st b_{1} is Heyting holds

( b_{1} is implicative & b_{1} is lower-bounded )
by Def5;

coherence

for b_{1} being Lattice st b_{1} is implicative & b_{1} is lower-bounded holds

b_{1} is Heyting
by Def5;

end;
for b

( b

coherence

for b

b

registration

ex b_{1} being Lattice st

( b_{1} is Heyting & b_{1} is strict )
end;

cluster non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like Heyting for LattStr ;

existence ex b

( b

proof end;

theorem :: LATTICE2:67

for L being 0_Lattice holds

( L is H_Lattice iff for x, z being Element of L ex y being Element of L st

( x "/\" y [= z & ( for v being Element of L st x "/\" v [= z holds

v [= y ) ) )

( L is H_Lattice iff for x, z being Element of L ex y being Element of L st

( x "/\" y [= z & ( for v being Element of L st x "/\" v [= z holds

v [= y ) ) )

proof end;

registration

coherence

for b_{1} being Lattice st b_{1} is finite holds

b_{1} is lower-bounded

for b_{1} being Lattice st b_{1} is finite holds

b_{1} is upper-bounded

end;
for b

b

proof end;

coherence for b

b

proof end;

registration

coherence

for b_{1} being Lattice st b_{1} is distributive & b_{1} is finite holds

b_{1} is Heyting

end;
for b

b

proof end;