:: Finite Join and Finite Meet, and Dual Lattices
:: 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
proofend;

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 )
proofend;

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
proofend;

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
proofend;

theorem Th5: :: LATTICE2:5
for f, g being Function st g c= f holds
f +* g = f
proofend;

theorem :: LATTICE2:6
for A being set
for C being non empty set
for B being Subset of A
for f being Function of A,C holds f +* (f | B) = f by Th5, RELAT_1:59;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

definition
let D be non empty set ;
let o, o9 be BinOp of D;
predo absorbs o9 means :Def1: :: LATTICE2:def 1
 for x, y being Element of D holds o . (x,(o9 . (x,y))) = x;
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 );

notation
let D be non empty set ;
let o, o9 be BinOp of D;
antonym o doesn't_absorb o9 for o absorbs o9;
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
proofend;

definition
let L be LattStr ;
funcL .:  ->  strict LattStr  equals :: LATTICE2:def 2
 LattStr(# the carrier of L, the L_meet of L, the L_join of L #);
correctness
coherence
LattStr(# the carrier of L, the L_meet of L, the L_join of L #) is strict LattStr ;
;
end;

:: 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 #);

registration
let L be non empty LattStr ;
clusterL .:  ->  non empty strict ;
coherence
 not L .: is empty ;
end;

theorem :: LATTICE2:12
for L being non empty LattStr holds
( the carrier of L = the carrier of (L .:) & the L_join of L = the L_meet of (L .:) & the L_meet of L = the L_join of (L .:) ) ;

theorem :: LATTICE2:13
for L being non empty strict LattStr holds (L .:) .: = L ;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

registration
let L be Lattice;
cluster the L_join of L ->  idempotent ;
coherence
 the L_join of L is idempotent
proofend;
end;

registration
let L be non empty join-commutative \/-SemiLattStr ;
cluster the L_join of L ->  commutative ;
coherence
 the L_join of L is commutative
proofend;
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
proofend;

registration
let L be non empty join-associative \/-SemiLattStr ;
cluster the L_join of L ->  associative ;
coherence
 the L_join of L is associative
proofend;
end;

registration
let L be Lattice;
cluster the L_meet of L ->  idempotent ;
coherence
 the L_meet of L is idempotent
proofend;
end;

registration
let L be non empty meet-commutative /\-SemiLattStr ;
cluster the L_meet of L ->  commutative ;
coherence
 the L_meet of L is commutative
proofend;
end;

registration
let L be non empty meet-associative /\-SemiLattStr ;
cluster the L_meet of L ->  associative ;
coherence
 the L_meet of L is associative
proofend;
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
proofend;

theorem Th20: :: LATTICE2:20
for L being Lattice holds the L_join of L is_distributive_wrt the L_join of L
proofend;

theorem :: LATTICE2:21
for L being Lattice st L is D_Lattice holds
the L_join of L is_distributive_wrt the L_meet of L
proofend;

theorem Th22: :: LATTICE2:22
for L being Lattice st the L_join of L is_distributive_wrt the L_meet of L holds
L is distributive
proofend;

theorem Th23: :: LATTICE2:23
for L being Lattice st L is D_Lattice holds
the L_meet of L is_distributive_wrt the L_join of L
proofend;

theorem :: LATTICE2:24
for L being Lattice st the L_meet of L is_distributive_wrt the L_join of L holds
L is distributive
proofend;

theorem Th25: :: LATTICE2:25
for L being Lattice holds the L_meet of L is_distributive_wrt the L_meet of L
proofend;

theorem Th26: :: LATTICE2:26
for L being Lattice holds the L_join of L absorbs the L_meet of L
proofend;

theorem Th27: :: LATTICE2:27
for L being Lattice holds the L_meet of L absorbs the L_join of L
proofend;

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;
func FinJoin (B,f) ->  Element of L equals :: LATTICE2:def 3
 the L_join of L $$ (B,f);
correctness
coherence
the L_join of L $$ (B,f) is Element of L;
;
func FinMeet (B,f) ->  Element of L equals :: LATTICE2:def 4
 the L_meet of L $$ (B,f);
correctness
coherence
the L_meet of L $$ (B,f) is Element of L;
;
end;

:: 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);

:: 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);

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)
proofend;

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)
proofend;

theorem :: LATTICE2:30
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 ( for x being Element of A st x in B holds
f . x = u ) &amp; B <> {} holds
FinJoin (B,f) = u by SETWISEO:24;

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
proofend;

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 <> {} &amp; ( for x being Element of A st x in B holds
f . x [= u ) holds
FinJoin (B,f) [= u
proofend;

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 <> {} &amp; ( for x being Element of A st x in B holds
f . x [= g . x ) holds
FinJoin (B,f) [= FinJoin (B,g)
proofend;

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 <> {} &amp; f | B = g | B holds
FinJoin (B,f) = FinJoin (B,g)
proofend;

theorem :: LATTICE2:35
for L being Lattice
for v 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 <> {} holds
v "\/" (FinJoin (B,f)) = FinJoin (B,( the L_join of L [;] (v,f))) by Th20, SETWISEO:27;

registration
let L be Lattice;
clusterL .:  ->  strict Lattice-like ;
coherence
 L .: is Lattice-like
proofend;
end;

theorem :: LATTICE2:36
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
for f9 being Function of A, the carrier of (L .:) st f = f9 holds
( FinJoin (B,f) = FinMeet (B,f9) &amp; FinMeet (B,f) = FinJoin (B,f9) ) ;

theorem Th37: :: LATTICE2:37
for L being Lattice
for a, b being Element of L
for a9, b9 being Element of (L .:) st a = a9 &amp; b = b9 holds
( a "/\" b = a9 "\/" b9 &amp; a "\/" b = a9 "/\" b9 ) ;

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 &amp; b = b9 holds
b9 [= a9
proofend;

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 &amp; a = a9 &amp; b = b9 holds
b [= a
proofend;

:: 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
proofend;

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 &amp; f . x [= u ) holds
FinMeet (B,f) [= u
proofend;

theorem :: LATTICE2:42
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 ( for x being Element of A st x in B holds
f . x = u ) &amp; B <> {} holds
FinMeet (B,f) = u by SETWISEO:24;

theorem :: LATTICE2:43
for L being Lattice
for v 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 <> {} holds
v "/\" (FinMeet (B,f)) = FinMeet (B,( the L_meet of L [;] (v,f))) by Th25, SETWISEO:27;

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
proofend;

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 <> {} &amp; f | B = g | B holds
FinMeet (B,f) = FinMeet (B,g)
proofend;

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 <> {} &amp; ( for x being Element of A st x in B holds
u [= f . x ) holds
u [= FinMeet (B,f)
proofend;

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 <> {} &amp; ( for x being Element of A st x in B holds
f . x [= g . x ) holds
FinMeet (B,f) [= FinMeet (B,g)
proofend;

theorem :: LATTICE2:48
for L being Lattice holds
( L is lower-bounded iff L .: is upper-bounded )
proofend;

theorem Th49: :: LATTICE2:49
for L being Lattice holds
( L is upper-bounded iff L .: is lower-bounded )
proofend;

theorem :: LATTICE2:50
for L being Lattice holds
( L is D_Lattice iff L .: is D_Lattice ) by Th22, Th23;

theorem Th51: :: LATTICE2:51
for L being 0_Lattice holds Bottom L is_a_unity_wrt the L_join of L
proofend;

registration
let L be 0_Lattice;
cluster the L_join of L ->  having_a_unity ;
coherence
 the L_join of L is having_a_unity
proofend;
end;

theorem :: LATTICE2:52
for L being 0_Lattice holds Bottom L = the_unity_wrt the L_join of L by Th18;

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)
proofend;

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
proofend;

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)
proofend;

theorem Th56: :: LATTICE2:56
for L being 1_Lattice holds Top L is_a_unity_wrt the L_meet of L
proofend;

registration
let L be 1_Lattice;
cluster the L_meet of L ->  having_a_unity ;
coherence
 the L_meet of L is having_a_unity
proofend;
end;

theorem :: LATTICE2:57
for L being 1_Lattice holds Top L = the_unity_wrt the L_meet of L by Th19;

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)
proofend;

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)
proofend;

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)
proofend;

theorem :: LATTICE2:61
for L being 0_Lattice holds Bottom L = Top (L .:)
proofend;

theorem :: LATTICE2:62
for L being 1_Lattice holds Top L = Bottom (L .:)
proofend;

::
:: Distributive lattices with the minimal element
::
definition
mode D0_Lattice is distributive lower-bounded Lattice;
end;

theorem :: LATTICE2:63
for L being D0_Lattice holds the L_meet of L is_distributive_wrt the L_join of L by Th23;

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)))
proofend;

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)
proofend;

theorem :: LATTICE2:66
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 u "/\" (FinJoin (B,f)) = FinJoin (B,( the L_meet of L [;] (u,f))) by Th64;

:: Heyting Lattices
definition
let IT be Lattice;
attrIT is Heyting  means :Def5: :: LATTICE2:def 5
( IT is implicative &amp; IT is lower-bounded );
end;

:: deftheorem Def5 defines Heyting LATTICE2:def_5_:_
 for IT being Lattice holds
( IT is Heyting iff ( IT is implicative &amp; IT is lower-bounded ) );

registration
cluster non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like Heyting for LattStr ;
existence
 ex b1 being Lattice st b1 is Heyting
proofend;
end;

registration
cluster non empty Lattice-like Heyting  ->  lower-bounded implicative for LattStr ;
coherence
 for b1 being Lattice st b1 is Heyting holds
( b1 is implicative &amp; b1 is lower-bounded ) by Def5;
cluster non empty Lattice-like lower-bounded implicative  ->  Heyting for LattStr ;
coherence
 for b1 being Lattice st b1 is implicative &amp; b1 is lower-bounded holds
b1 is Heyting by Def5;
end;

definition
mode H_Lattice is Heyting Lattice;
end;

registration
cluster non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like Heyting for LattStr ;
existence
 ex b1 being Lattice st
( b1 is Heyting &amp; b1 is strict )
proofend;
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 &amp; ( for v being Element of L st x "/\" v [= z holds
v [= y ) ) )
proofend;

theorem :: LATTICE2:68
for L being Lattice holds
( L is finite iff L .: is finite ) ;

registration
cluster non empty finite Lattice-like  ->  lower-bounded for LattStr ;
coherence
 for b1 being Lattice st b1 is finite holds
b1 is lower-bounded
proofend;
cluster non empty finite Lattice-like  ->  upper-bounded for LattStr ;
coherence
 for b1 being Lattice st b1 is finite holds
b1 is upper-bounded
proofend;
end;

registration
cluster non empty finite Lattice-like  ->  bounded for LattStr ;
coherence
 for b1 being Lattice st b1 is finite holds
b1 is bounded ;
end;

registration
cluster non empty finite Lattice-like distributive  ->  Heyting for LattStr ;
coherence
 for b1 being Lattice st b1 is distributive &amp; b1 is finite holds
b1 is Heyting
proofend;
end;