:: Formalization of Generalized Almost Distributive Lattices
:: by Adam Grabowski
::
:: Received September 26, 2014
:: Copyright (c) 2014-2021 Association of Mizar Users


theorem Ble1: :: LATTAD_1:1
for L being non empty 1-sorted
for R being total Relation of the carrier of L holds
( R is reflexive iff for x being Element of L holds [x,x] in R )
proof end;

registration
cluster non empty trivial -> non empty distributive for LattStr ;
coherence
for b1 being non empty LattStr st b1 is trivial holds
b1 is distributive
;
end;

:: Almost Distributive Lattices satisfy:
:: a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c);
:: (x \/ y) /\ z = (x /\ z) \/ (y /\ z)
:: (x \/ y) /\ y = y
:: (x \/ y) /\ x = x
:: x \/ (x /\ y) = x (meet-Absorbing)
definition
let L be non empty LattStr ;
:: Almost Distributive Lattices satisfy:
:: a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c);
:: (x \/ y) /\ z = (x /\ z) \/ (y /\ z)
:: (x \/ y) /\ y = y
:: (x \/ y) /\ x = x
:: x \/ (x /\ y) = x (meet-Absorbing)
attr L is Distributive means :DefD: :: LATTAD_1:def 1
for x, y, z being Element of L holds (x "\/" y) "/\" z = (x "/\" z) "\/" (y "/\" z);
attr L is Meet-absorbing means :DefA1: :: LATTAD_1:def 2
for x, y being Element of L holds (x "\/" y) "/\" y = y;
attr L is Meet-Absorbing means :DefA2: :: LATTAD_1:def 3
for x, y being Element of L holds (x "\/" y) "/\" x = x;
end;

:: deftheorem DefD defines Distributive LATTAD_1:def 1 :
for L being non empty LattStr holds
( L is Distributive iff for x, y, z being Element of L holds (x "\/" y) "/\" z = (x "/\" z) "\/" (y "/\" z) );

:: deftheorem DefA1 defines Meet-absorbing LATTAD_1:def 2 :
for L being non empty LattStr holds
( L is Meet-absorbing iff for x, y being Element of L holds (x "\/" y) "/\" y = y );

:: deftheorem DefA2 defines Meet-Absorbing LATTAD_1:def 3 :
for L being non empty LattStr holds
( L is Meet-Absorbing iff for x, y being Element of L holds (x "\/" y) "/\" x = x );

registration
cluster non empty trivial -> non empty meet-Absorbing Distributive Meet-absorbing Meet-Absorbing for LattStr ;
coherence
for b1 being non empty LattStr st b1 is trivial holds
( b1 is Distributive & b1 is Meet-absorbing & b1 is Meet-Absorbing & b1 is meet-Absorbing )
;
cluster non empty trivial -> non empty Lattice-like for LattStr ;
coherence
for b1 being non empty LattStr st b1 is trivial holds
b1 is Lattice-like
proof end;
end;

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

registration
cluster non empty distributive meet-Absorbing Distributive Meet-absorbing Meet-Absorbing for LattStr ;
existence
ex b1 being non empty LattStr st
( b1 is Distributive & b1 is distributive & b1 is Meet-absorbing & b1 is Meet-Absorbing & b1 is meet-Absorbing )
proof end;
end;

definition
mode AD_Lattice is non empty distributive meet-Absorbing Distributive Meet-absorbing Meet-Absorbing LattStr ;
end;

theorem :: LATTAD_1:2
for L being AD_Lattice
for x, y being Element of L holds
( x "\/" y = x iff x "/\" y = y ) by DefA1, ROBBINS3:def 3;

theorem ISum: :: LATTAD_1:3
for L being AD_Lattice
for x being Element of L holds x "\/" x = x
proof end;

theorem IMeet: :: LATTAD_1:4
for L being AD_Lattice
for x being Element of L holds x "/\" x = x
proof end;

theorem LemXX: :: LATTAD_1:5
for L being AD_Lattice
for x, y being Element of L holds (x "/\" y) "\/" y = y
proof end;

theorem Lem232: :: LATTAD_1:6
for L being AD_Lattice
for x, y being Element of L holds
( x "\/" y = y iff x "/\" y = x )
proof end;

theorem Ze: :: LATTAD_1:7
for L being AD_Lattice
for x, y being Element of L holds x "/\" (x "\/" y) = x
proof end;

theorem :: LATTAD_1:8
for L being AD_Lattice
for x, y being Element of L holds x "\/" (y "/\" x) = x
proof end;

theorem :: LATTAD_1:9
for L being AD_Lattice
for x, y being Element of L holds
( x [= x "\/" y & x "/\" y [= y )
proof end;

theorem :: LATTAD_1:10
for L being AD_Lattice
for x, y being Element of L holds
( x [= y iff x "/\" y = x ) by Lem232;

theorem Lem36c: :: LATTAD_1:11
for L being AD_Lattice
for x, y being Element of L holds x "/\" (y "/\" x) = y "/\" x
proof end;

theorem Th1712: :: LATTAD_1:12
for L being AD_Lattice
for x, y being Element of L holds
( (x "/\" y) "\/" x = x iff x "/\" (y "\/" x) = x )
proof end;

theorem :: LATTAD_1:13
for L being AD_Lattice
for x, y being Element of L holds
( (y "/\" x) "\/" y = y iff y "/\" (x "\/" y) = y ) by Th1712;

theorem :: LATTAD_1:14
for L being AD_Lattice
for x, y being Element of L st (x "/\" y) "\/" x = x holds
x "/\" y = y "/\" x
proof end;

theorem Th1726: :: LATTAD_1:15
for L being AD_Lattice
for x, y being Element of L st x "/\" (y "\/" x) = x holds
x "\/" y = y "\/" x
proof end;

theorem Hehe1: :: LATTAD_1:16
for L being AD_Lattice
for x, y being Element of L st ex z being Element of L st
( x [= z & y [= z ) holds
x "\/" y = y "\/" x
proof end;

theorem :: LATTAD_1:17
for L being AD_Lattice
for x, y being Element of L st x [= y holds
x "\/" y = y "\/" x
proof end;

:: A Generalized Almost Distributive Lattice satisfies:
::
:: (x /\ y) /\ z = x /\ (y /\ z)
:: x /\ (y \/ z) = (x /\ y) \/ (x /\ z) (distributive)
:: x \/ (y /\ z) = (x \/ y) /\ (x \/ z)
:: x /\ (x \/ y) = x (join-absorbing)
:: (x \/ y) /\ x = x (Meet-Absorbing)
:: (x /\ y) \/ y = y (meet-absorbing)
definition
let L be non empty LattStr ;
:: A Generalized Almost Distributive Lattice satisfies:
::
:: (x /\ y) /\ z = x /\ (y /\ z)
:: x /\ (y \/ z) = (x /\ y) \/ (x /\ z) (distributive)
:: x \/ (y /\ z) = (x \/ y) /\ (x \/ z)
:: x /\ (x \/ y) = x (join-absorbing)
:: (x \/ y) /\ x = x (Meet-Absorbing)
:: (x /\ y) \/ y = y (meet-absorbing)
attr L is left-Distributive means :DefLDS: :: LATTAD_1:def 4
for x, y, z being Element of L holds x "\/" (y "/\" z) = (x "\/" y) "/\" (x "\/" z);
attr L is ADL-absorbing means :: LATTAD_1:def 5
for x, y being Element of L holds x "/\" (y "\/" x) = x;
end;

:: deftheorem DefLDS defines left-Distributive LATTAD_1:def 4 :
for L being non empty LattStr holds
( L is left-Distributive iff for x, y, z being Element of L holds x "\/" (y "/\" z) = (x "\/" y) "/\" (x "\/" z) );

:: deftheorem defines ADL-absorbing LATTAD_1:def 5 :
for L being non empty LattStr holds
( L is ADL-absorbing iff for x, y being Element of L holds x "/\" (y "\/" x) = x );

registration
cluster non empty trivial -> non empty meet-associative distributive Meet-Absorbing left-Distributive for LattStr ;
coherence
for b1 being non empty LattStr st b1 is trivial holds
( b1 is meet-associative & b1 is distributive & b1 is left-Distributive & b1 is Meet-Absorbing )
;
end;

registration
cluster non empty meet-associative meet-absorbing join-absorbing distributive Meet-Absorbing left-Distributive for LattStr ;
existence
ex b1 being non empty LattStr st
( b1 is meet-associative & b1 is distributive & b1 is left-Distributive & b1 is join-absorbing & b1 is Meet-Absorbing & b1 is meet-absorbing )
proof end;
end;

definition
mode GAD_Lattice is non empty meet-associative meet-absorbing join-absorbing distributive Meet-Absorbing left-Distributive LattStr ;
end;

theorem ISum: :: LATTAD_1:18
for L being GAD_Lattice
for x being Element of L holds x "\/" x = x
proof end;

theorem IMeet: :: LATTAD_1:19
for L being GAD_Lattice
for x being Element of L holds x "/\" x = x
proof end;

theorem ThA4: :: LATTAD_1:20
for L being GAD_Lattice
for x, y being Element of L holds x "\/" (x "/\" y) = x
proof end;

theorem ThA5: :: LATTAD_1:21
for L being GAD_Lattice
for x, y being Element of L holds x "\/" (y "/\" x) = x
proof end;

theorem :: LATTAD_1:22
for L being GAD_Lattice
for x, y being Element of L st x "/\" y = y holds
x "\/" y = x by ThA4;

theorem :: LATTAD_1:23
for L being GAD_Lattice
for x, y being Element of L holds
( x "\/" y = y iff x "/\" y = x ) by LATTICES:def 9, LATTICES:def 8;

theorem Idem: :: LATTAD_1:24
for L being GAD_Lattice
for x being Element of L holds x [= x
proof end;

theorem TransLat: :: LATTAD_1:25
for L being GAD_Lattice
for x, y, z being Element of L st x [= y & y [= z holds
x [= z
proof end;

definition
let L be non empty LattStr ;
::: LattRel could be used, if generalized - TODO
func LatOrder L -> Relation equals :: LATTAD_1:def 6
{ [a,b] where a, b is Element of L : a [= b } ;
coherence
{ [a,b] where a, b is Element of L : a [= b } is Relation
proof end;
end;

:: deftheorem defines LatOrder LATTAD_1:def 6 :
for L being non empty LattStr holds LatOrder L = { [a,b] where a, b is Element of L : a [= b } ;

theorem Th32: :: LATTAD_1:26
for L being GAD_Lattice holds
( dom (LatOrder L) = the carrier of L & rng (LatOrder L) = the carrier of L & field (LatOrder L) = the carrier of L )
proof end;

definition
let L be GAD_Lattice;
:: original: LatOrder
redefine func LatOrder L -> Relation of the carrier of L;
correctness
coherence
LatOrder L is Relation of the carrier of L
;
proof end;
end;

registration
let L be GAD_Lattice;
cluster LatOrder L -> total for Relation of the carrier of L;
correctness
coherence
for b1 being Relation of the carrier of L st b1 = LatOrder L holds
b1 is total
;
proof end;
end;

theorem OrdLat: :: LATTAD_1:27
for L being GAD_Lattice
for x, y being Element of L holds
( [x,y] in LatOrder L iff x [= y )
proof end;

definition
let L be non empty LattStr ;
func ThetaOrder L -> Relation equals :: LATTAD_1:def 7
{ [a,b] where a, b is Element of L : a "/\" b = b } ;
coherence
{ [a,b] where a, b is Element of L : a "/\" b = b } is Relation
proof end;
end;

:: deftheorem defines ThetaOrder LATTAD_1:def 7 :
for L being non empty LattStr holds ThetaOrder L = { [a,b] where a, b is Element of L : a "/\" b = b } ;

theorem Th32: :: LATTAD_1:28
for L being GAD_Lattice holds
( dom (ThetaOrder L) = the carrier of L & rng (ThetaOrder L) = the carrier of L & field (ThetaOrder L) = the carrier of L )
proof end;

definition
let L be GAD_Lattice;
:: original: ThetaOrder
redefine func ThetaOrder L -> Relation of the carrier of L;
correctness
coherence
ThetaOrder L is Relation of the carrier of L
;
proof end;
end;

registration
let L be GAD_Lattice;
cluster ThetaOrder L -> total for Relation of the carrier of L;
correctness
coherence
for b1 being Relation of the carrier of L st b1 = ThetaOrder L holds
b1 is total
;
proof end;
end;

theorem ThetaOrdLat: :: LATTAD_1:29
for L being GAD_Lattice
for x, y being Element of L holds
( [x,y] in ThetaOrder L iff x "/\" y = y )
proof end;

registration
let L be GAD_Lattice;
cluster LatOrder L -> reflexive ;
coherence
LatOrder L is reflexive
proof end;
cluster LatOrder L -> transitive ;
coherence
LatOrder L is transitive
proof end;
end;

registration
let L be GAD_Lattice;
cluster ThetaOrder L -> reflexive ;
coherence
ThetaOrder L is reflexive
proof end;
cluster ThetaOrder L -> transitive ;
coherence
ThetaOrder L is transitive
proof end;
end;

theorem Lem36X: :: LATTAD_1:30
for L being GAD_Lattice
for x, y being Element of L holds x "\/" (x "\/" y) = x "\/" y
proof end;

theorem Lem36c: :: LATTAD_1:31
for L being GAD_Lattice
for x, y being Element of L holds x "/\" (y "/\" x) = y "/\" x
proof end;

theorem :: LATTAD_1:32
for L being GAD_Lattice
for x, y being Element of L holds y "/\" (x "/\" y) = x "/\" y by Lem36c;

Th3715: for L being GAD_Lattice
for x, y being Element of L st (x "/\" y) "\/" x = x holds
x "/\" y = y "/\" x

proof end;

Th3713: for L being GAD_Lattice
for x, y being Element of L st (x "/\" y) "\/" x = x holds
(y "/\" x) "\/" y = y

proof end;

Th3712: for L being GAD_Lattice
for x, y being Element of L holds
( (x "/\" y) "\/" x = x iff x "/\" (y "\/" x) = x )

proof end;

Th3726: for L being GAD_Lattice
for x, y being Element of L st x "/\" (y "\/" x) = x holds
x "\/" y = y "\/" x

proof end;

DefB2: for L being GAD_Lattice
for a, b being Element of L st ex c being Element of L st
( a [= c & b [= c ) holds
a "\/" b = b "\/" a

proof end;

definition
let L be GAD_Lattice;
let a, b be Element of L;
pred ex_lub_of a,b means :: LATTAD_1:def 8
ex c being Element of L st
( a [= c & b [= c & ( for x being Element of L st a [= x & b [= x holds
c [= x ) );
pred ex_glb_of a,b means :: LATTAD_1:def 9
ex c being Element of L st
( c [= a & c [= b & ( for x being Element of L st x [= a & x [= b holds
x [= c ) );
end;

:: deftheorem defines ex_lub_of LATTAD_1:def 8 :
for L being GAD_Lattice
for a, b being Element of L holds
( ex_lub_of a,b iff ex c being Element of L st
( a [= c & b [= c & ( for x being Element of L st a [= x & b [= x holds
c [= x ) ) );

:: deftheorem defines ex_glb_of LATTAD_1:def 9 :
for L being GAD_Lattice
for a, b being Element of L holds
( ex_glb_of a,b iff ex c being Element of L st
( c [= a & c [= b & ( for x being Element of L st x [= a & x [= b holds
x [= c ) ) );

definition
let L be GAD_Lattice;
let a, b be Element of L;
assume A1: ex_lub_of a,b ;
func lub (a,b) -> Element of L means :DefLUB: :: LATTAD_1:def 10
( a [= it & b [= it & ( for x being Element of L st a [= x & b [= x holds
it [= x ) );
existence
ex b1 being Element of L st
( a [= b1 & b [= b1 & ( for x being Element of L st a [= x & b [= x holds
b1 [= x ) )
by A1;
correctness
uniqueness
for b1, b2 being Element of L st a [= b1 & b [= b1 & ( for x being Element of L st a [= x & b [= x holds
b1 [= x ) & a [= b2 & b [= b2 & ( for x being Element of L st a [= x & b [= x holds
b2 [= x ) holds
b1 = b2
;
proof end;
end;

:: deftheorem DefLUB defines lub LATTAD_1:def 10 :
for L being GAD_Lattice
for a, b being Element of L st ex_lub_of a,b holds
for b4 being Element of L holds
( b4 = lub (a,b) iff ( a [= b4 & b [= b4 & ( for x being Element of L st a [= x & b [= x holds
b4 [= x ) ) );

definition
let L be GAD_Lattice;
let a, b be Element of L;
assume A1: ex_glb_of a,b ;
func glb (a,b) -> Element of L means :DefGLB: :: LATTAD_1:def 11
( it [= a & it [= b & ( for x being Element of L st x [= a & x [= b holds
x [= it ) );
existence
ex b1 being Element of L st
( b1 [= a & b1 [= b & ( for x being Element of L st x [= a & x [= b holds
x [= b1 ) )
by A1;
correctness
uniqueness
for b1, b2 being Element of L st b1 [= a & b1 [= b & ( for x being Element of L st x [= a & x [= b holds
x [= b1 ) & b2 [= a & b2 [= b & ( for x being Element of L st x [= a & x [= b holds
x [= b2 ) holds
b1 = b2
;
proof end;
end;

:: deftheorem DefGLB defines glb LATTAD_1:def 11 :
for L being GAD_Lattice
for a, b being Element of L st ex_glb_of a,b holds
for b4 being Element of L holds
( b4 = glb (a,b) iff ( b4 [= a & b4 [= b & ( for x being Element of L st x [= a & x [= b holds
x [= b4 ) ) );

Th3751: for L being GAD_Lattice
for x, y being Element of L st x "/\" y = y "/\" x holds
(x "/\" y) "\/" x = x

by LATTICES:def 8;

IffComm: for L being GAD_Lattice
for x, y being Element of L st x "\/" y = y "\/" x holds
x "/\" y = y "/\" x

proof end;

:: Theorem 3.7.
theorem :: LATTAD_1:33
for L being GAD_Lattice
for x, y being Element of L holds
( (x "/\" y) "\/" x = x iff x "/\" (y "\/" x) = x ) by Th3712;

theorem :: LATTAD_1:34
for L being GAD_Lattice
for x, y being Element of L holds
( (x "/\" y) "\/" x = x iff (y "/\" x) "\/" y = y ) by Th3713;

theorem :: LATTAD_1:35
for L being GAD_Lattice
for x, y being Element of L holds
( (x "/\" y) "\/" x = x iff y "/\" (x "\/" y) = y )
proof end;

theorem :: LATTAD_1:36
for L being GAD_Lattice
for x, y being Element of L holds
( (x "/\" y) "\/" x = x iff x "/\" y = y "/\" x ) by Th3715, LATTICES:def 8;

theorem Th3716: :: LATTAD_1:37
for L being GAD_Lattice
for x, y being Element of L holds
( (x "/\" y) "\/" x = x iff x "\/" y = y "\/" x )
proof end;

theorem :: LATTAD_1:38
for L being GAD_Lattice
for x, y being Element of L holds
( x [= y iff x "/\" y = x ) by LATTICES:def 9, LATTICES:def 8;

LemX3: for L being GAD_Lattice
for x, y being Element of L holds x [= x "\/" y

proof end;

LemB1: for L being GAD_Lattice
for x, y being Element of L holds x "/\" y [= y

by LATTICES:def 8;

Th3823: for L being GAD_Lattice
for x, y being Element of L st y [= x "\/" y holds
ex z being Element of L st
( x [= z & y [= z )

proof end;

Th3851: for L being GAD_Lattice
for x, y being Element of L st x [= y "\/" x holds
x "\/" y = y "\/" x

proof end;

Th3856: for L being GAD_Lattice
for x, y being Element of L st x [= y "\/" x holds
( ex_lub_of x,y & y "\/" x = lub (x,y) )

proof end;

Th3865: for L being GAD_Lattice
for x, y being Element of L st ex_lub_of x,y & y "\/" x = lub (x,y) holds
x [= y "\/" x

by DefLUB;

Th3834: for L being GAD_Lattice
for x, y being Element of L st ex c being Element of L st
( x [= c & y [= c ) holds
( ex_lub_of x,y & x "\/" y = lub (x,y) )

proof end;

Th3841: for L being GAD_Lattice
for x, y being Element of L st ex_lub_of x,y & x "\/" y = lub (x,y) holds
x "\/" y = y "\/" x

proof end;

:: Theorem 3.8.
theorem :: LATTAD_1:39
for L being GAD_Lattice
for x, y being Element of L holds
( x "\/" y = y "\/" x iff y [= x "\/" y )
proof end;

theorem :: LATTAD_1:40
for L being GAD_Lattice
for x, y being Element of L holds
( x "\/" y = y "\/" x iff ex z being Element of L st
( x [= z & y [= z ) ) by Th3823, LemX3, DefB2;

theorem Th381i4: :: LATTAD_1:41
for L being GAD_Lattice
for x, y being Element of L holds
( x "\/" y = y "\/" x iff ( ex_lub_of x,y & x "\/" y = lub (x,y) ) )
proof end;

theorem :: LATTAD_1:42
for L being GAD_Lattice
for x, y being Element of L holds
( x "\/" y = y "\/" x iff x [= y "\/" x ) by LemX3, Th3851;

theorem :: LATTAD_1:43
for L being GAD_Lattice
for x, y being Element of L holds
( x "\/" y = y "\/" x iff ( ex_lub_of x,y & y "\/" x = lub (x,y) ) )
proof end;

Lm1: now :: thesis: for L being GAD_Lattice
for a, b being Element of L st L is join-commutative holds
for c being Element of L holds
( c = a "\/" b iff ( a [= c & b [= c & ( for d being Element of L st a [= d & b [= d holds
c [= d ) ) )
let L be GAD_Lattice; :: thesis: for a, b being Element of L st L is join-commutative holds
for c being Element of L holds
( c = a "\/" b iff ( a [= c & b [= c & ( for d being Element of L st a [= d & b [= d holds
c [= d ) ) )

let a, b be Element of L; :: thesis: ( L is join-commutative implies for c being Element of L holds
( c = a "\/" b iff ( a [= c & b [= c & ( for d being Element of L st a [= d & b [= d holds
c [= d ) ) ) )

assume ZZ: L is join-commutative ; :: thesis: for c being Element of L holds
( c = a "\/" b iff ( a [= c & b [= c & ( for d being Element of L st a [= d & b [= d holds
c [= d ) ) )

Z1: for x, y being Element of L holds
( ex_lub_of x,y & x "\/" y = lub (x,y) )
proof
let x, y be Element of L; :: thesis: ( ex_lub_of x,y & x "\/" y = lub (x,y) )
x "\/" y = y "\/" x by ZZ;
hence ( ex_lub_of x,y & x "\/" y = lub (x,y) ) by Th381i4; :: thesis: verum
end;
S1: ( ex_lub_of a,b & a "\/" b = lub (a,b) ) by Z1;
let c be Element of L; :: thesis: ( c = a "\/" b iff ( a [= c & b [= c & ( for d being Element of L st a [= d & b [= d holds
c [= d ) ) )

thus ( c = a "\/" b iff ( a [= c & b [= c & ( for d being Element of L st a [= d & b [= d holds
c [= d ) ) ) by S1, DefLUB; :: thesis: verum
end;

Th14: for L being GAD_Lattice st L is join-commutative holds
for u1, u2, u3 being Element of L holds (u1 "\/" u2) "\/" u3 = u1 "\/" (u2 "\/" u3)

proof end;

:: Theorem 3.9.
theorem :: LATTAD_1:44
for L being GAD_Lattice
for x, y being Element of L st x "/\" y [= x holds
ex z being Element of L st
( z [= x & z [= y ) by LemB1;

theorem Th391i4: :: LATTAD_1:45
for L being GAD_Lattice
for x, y being Element of L holds
( x "/\" y = y "/\" x iff y "/\" x [= y ) by LATTICES:def 8, Th3715;

Th3956: for L being GAD_Lattice
for x, y being Element of L st y "/\" x [= y holds
( ex_glb_of x,y & y "/\" x = glb (x,y) )

proof end;

Th3965: for L being GAD_Lattice
for x, y being Element of L st ex_glb_of x,y & y "/\" x = glb (x,y) holds
y "/\" x [= y

by DefGLB;

theorem :: LATTAD_1:46
for L being GAD_Lattice
for x, y being Element of L holds
( x "/\" y = y "/\" x iff ( ex_glb_of x,y & y "/\" x = glb (x,y) ) )
proof end;

theorem :: LATTAD_1:47
for L being GAD_Lattice
for x, y being Element of L holds
( x "/\" y = y "/\" x iff x "/\" y [= x ) by LATTICES:def 8, Th3715;

ThXXX: for L being GAD_Lattice
for x, y being Element of L st x "/\" y [= x holds
( ex_glb_of x,y & x "/\" y = glb (x,y) )

proof end;

theorem :: LATTAD_1:48
for L being GAD_Lattice
for x, y being Element of L holds
( x "/\" y = y "/\" x iff ( ex_glb_of x,y & x "/\" y = glb (x,y) ) )
proof end;

theorem Lem310: :: LATTAD_1:49
for L being GAD_Lattice
for x, y, z being Element of L holds (x "/\" y) "/\" z = (y "/\" x) "/\" z
proof end;

definition
let L be GAD_Lattice;
func LatRelStr L -> strict RelStr equals :: LATTAD_1:def 12
RelStr(# the carrier of L,(LatOrder L) #);
coherence
RelStr(# the carrier of L,(LatOrder L) #) is strict RelStr
;
end;

:: deftheorem defines LatRelStr LATTAD_1:def 12 :
for L being GAD_Lattice holds LatRelStr L = RelStr(# the carrier of L,(LatOrder L) #);

registration
let L be GAD_Lattice;
cluster LatRelStr L -> strict reflexive transitive ;
coherence
( LatRelStr L is reflexive & LatRelStr L is transitive )
;
end;

theorem :: LATTAD_1:50
for L being GAD_Lattice
for a, b being Element of L
for x, y being Element of (LatRelStr L) st a = x & b = y holds
( x <= y iff a [= b ) by OrdLat, ORDERS_2:def 5;

Th31145: for L being GAD_Lattice holds
( L is join-commutative iff L is meet-commutative )

proof end;

theorem Th31141: :: LATTAD_1:51
for L being GAD_Lattice holds
( L is join-commutative iff ( L is Lattice-like & L is distributive ) )
proof end;

theorem :: LATTAD_1:52
for L being GAD_Lattice holds
( L is join-commutative iff LatRelStr L is directed )
proof end;

theorem Th31143: :: LATTAD_1:53
for L being GAD_Lattice holds
( L is join-commutative iff L is ADL-absorbing )
proof end;

theorem :: LATTAD_1:54
for L being GAD_Lattice holds
( L is join-commutative iff L is meet-commutative ) by Th31145;

theorem Th31146: :: LATTAD_1:55
for L being GAD_Lattice holds
( L is join-commutative iff ThetaOrder L is antisymmetric )
proof end;

theorem :: LATTAD_1:56
for L being GAD_Lattice holds
( L is join-commutative iff ThetaOrder L is being_partial-order )
proof end;

registration
let L be join-commutative GAD_Lattice;
cluster ThetaOrder L -> antisymmetric ;
coherence
ThetaOrder L is antisymmetric
by Th31146;
end;

registration
cluster non empty join-commutative meet-associative meet-absorbing join-absorbing distributive Meet-Absorbing left-Distributive -> ADL-absorbing for LattStr ;
coherence
for b1 being GAD_Lattice st b1 is join-commutative holds
b1 is ADL-absorbing
by Th31143;
cluster non empty meet-associative meet-absorbing join-absorbing distributive Meet-Absorbing left-Distributive ADL-absorbing -> join-commutative for LattStr ;
coherence
for b1 being GAD_Lattice st b1 is ADL-absorbing holds
b1 is join-commutative
by Th31143;
end;

registration
cluster non empty join-commutative meet-associative meet-absorbing join-absorbing distributive Meet-Absorbing left-Distributive -> meet-commutative for LattStr ;
coherence
for b1 being GAD_Lattice st b1 is join-commutative holds
b1 is meet-commutative
by Th31145;
cluster non empty meet-commutative meet-associative meet-absorbing join-absorbing distributive Meet-Absorbing left-Distributive -> join-commutative for LattStr ;
coherence
for b1 being GAD_Lattice st b1 is meet-commutative holds
b1 is join-commutative
by Th31145;
end;

:: Theorem 3.13.
theorem :: LATTAD_1:57
for L being GAD_Lattice st ( for a, b, c being Element of L holds (a "\/" b) "/\" c = (b "\/" a) "/\" c ) holds
for a, b, c being Element of L holds (a "\/" b) "/\" c = (a "/\" c) "\/" (b "/\" c)
proof end;

theorem :: LATTAD_1:58
for L being GAD_Lattice st ( for a, b, c being Element of L holds (a "\/" b) "/\" c = (a "/\" c) "\/" (b "/\" c) ) holds
for a, b being Element of L holds (a "\/" b) "/\" b = b
proof end;

theorem :: LATTAD_1:59
for L being GAD_Lattice st ( for a, b being Element of L holds (a "\/" b) "/\" b = b ) holds
for a, b, c being Element of L holds (a "\/" b) "/\" c = (b "\/" a) "/\" c
proof end;

definition
let L be GAD_Lattice;
attr L is with_zero means :: LATTAD_1:def 13
ex x being Element of L st
for a being Element of L holds x "/\" a = x;
end;

:: deftheorem defines with_zero LATTAD_1:def 13 :
for L being GAD_Lattice holds
( L is with_zero iff ex x being Element of L st
for a being Element of L holds x "/\" a = x );

registration
cluster non empty trivial meet-associative meet-absorbing join-absorbing distributive Meet-Absorbing left-Distributive -> with_zero for LattStr ;
coherence
for b1 being GAD_Lattice st b1 is trivial holds
b1 is with_zero
proof end;
end;

registration
cluster non empty meet-associative meet-absorbing join-absorbing distributive Meet-Absorbing left-Distributive with_zero for LattStr ;
existence
ex b1 being GAD_Lattice st b1 is with_zero
proof end;
end;

definition
let L be GAD_Lattice;
assume A1: L is with_zero ;
func bottom L -> Element of L means :GADL0: :: LATTAD_1:def 14
for a being Element of L holds it "/\" a = it;
existence
ex b1 being Element of L st
for a being Element of L holds b1 "/\" a = b1
by A1;
uniqueness
for b1, b2 being Element of L st ( for a being Element of L holds b1 "/\" a = b1 ) & ( for a being Element of L holds b2 "/\" a = b2 ) holds
b1 = b2
proof end;
end;

:: deftheorem GADL0 defines bottom LATTAD_1:def 14 :
for L being GAD_Lattice st L is with_zero holds
for b2 being Element of L holds
( b2 = bottom L iff for a being Element of L holds b2 "/\" a = b2 );

theorem :: LATTAD_1:60
for L being with_zero GAD_Lattice
for x being Element of L holds x "\/" (bottom L) = x
proof end;

theorem :: LATTAD_1:61
for L being with_zero GAD_Lattice
for x being Element of L holds (bottom L) "\/" x = x
proof end;

theorem :: LATTAD_1:62
for L being with_zero GAD_Lattice
for x being Element of L holds x "/\" (bottom L) = bottom L
proof end;

theorem Lem316: :: LATTAD_1:63
for L being with_zero GAD_Lattice
for x, y being Element of L holds
( x "/\" y = bottom L iff y "/\" x = bottom L )
proof end;

theorem :: LATTAD_1:64
for L being with_zero GAD_Lattice
for x, y being Element of L st x "/\" y = bottom L holds
x "\/" y = y "\/" x
proof end;

Lmx2: ex x being Element of {1,2,3} st x = 1
proof end;

definition
let x, y be Element of {1,2,3};
func x example32"/\" y -> Element of {1,2,3} equals :Defx5: :: LATTAD_1:def 15
1 if ( y = 1 or ( y = 2 & ( x = 1 or x = 3 ) ) )
2 if ( x = 2 & y = 2 )
3 if y = 3
;
coherence
( ( ( y = 1 or ( y = 2 & ( x = 1 or x = 3 ) ) ) implies 1 is Element of {1,2,3} ) & ( x = 2 & y = 2 implies 2 is Element of {1,2,3} ) & ( y = 3 implies 3 is Element of {1,2,3} ) )
by Lmx2;
consistency
for b1 being Element of {1,2,3} holds
( ( ( y = 1 or ( y = 2 & ( x = 1 or x = 3 ) ) ) & x = 2 & y = 2 implies ( b1 = 1 iff b1 = 2 ) ) & ( ( y = 1 or ( y = 2 & ( x = 1 or x = 3 ) ) ) & y = 3 implies ( b1 = 1 iff b1 = 3 ) ) & ( x = 2 & y = 2 & y = 3 implies ( b1 = 2 iff b1 = 3 ) ) )
;
func x example32"\/" y -> Element of {1,2,3} equals :Defx6: :: LATTAD_1:def 16
1 if ( x = 1 & ( y = 1 or y = 3 ) )
2 if ( x = 2 or ( x = 1 & y = 2 ) )
3 if x = 3
;
coherence
( ( x = 1 & ( y = 1 or y = 3 ) implies 1 is Element of {1,2,3} ) & ( ( x = 2 or ( x = 1 & y = 2 ) ) implies 2 is Element of {1,2,3} ) & ( x = 3 implies 3 is Element of {1,2,3} ) )
;
consistency
for b1 being Element of {1,2,3} holds
( ( x = 1 & ( y = 1 or y = 3 ) & ( x = 2 or ( x = 1 & y = 2 ) ) implies ( b1 = 1 iff b1 = 2 ) ) & ( x = 1 & ( y = 1 or y = 3 ) & x = 3 implies ( b1 = 1 iff b1 = 3 ) ) & ( ( x = 2 or ( x = 1 & y = 2 ) ) & x = 3 implies ( b1 = 2 iff b1 = 3 ) ) )
;
end;

:: deftheorem Defx5 defines example32"/\" LATTAD_1:def 15 :
for x, y being Element of {1,2,3} holds
( ( ( y = 1 or ( y = 2 & ( x = 1 or x = 3 ) ) ) implies x example32"/\" y = 1 ) & ( x = 2 & y = 2 implies x example32"/\" y = 2 ) & ( y = 3 implies x example32"/\" y = 3 ) );

:: deftheorem Defx6 defines example32"\/" LATTAD_1:def 16 :
for x, y being Element of {1,2,3} holds
( ( x = 1 & ( y = 1 or y = 3 ) implies x example32"\/" y = 1 ) & ( ( x = 2 or ( x = 1 & y = 2 ) ) implies x example32"\/" y = 2 ) & ( x = 3 implies x example32"\/" y = 3 ) );

definition
func example32\/ -> BinOp of {1,2,3} means :Defx7: :: LATTAD_1:def 17
for x, y being Element of {1,2,3} holds it . (x,y) = x example32"\/" y;
existence
ex b1 being BinOp of {1,2,3} st
for x, y being Element of {1,2,3} holds b1 . (x,y) = x example32"\/" y
proof end;
uniqueness
for b1, b2 being BinOp of {1,2,3} st ( for x, y being Element of {1,2,3} holds b1 . (x,y) = x example32"\/" y ) & ( for x, y being Element of {1,2,3} holds b2 . (x,y) = x example32"\/" y ) holds
b1 = b2
proof end;
func example32/\ -> BinOp of {1,2,3} means :Defx8: :: LATTAD_1:def 18
for x, y being Element of {1,2,3} holds it . (x,y) = x example32"/\" y;
existence
ex b1 being BinOp of {1,2,3} st
for x, y being Element of {1,2,3} holds b1 . (x,y) = x example32"/\" y
proof end;
uniqueness
for b1, b2 being BinOp of {1,2,3} st ( for x, y being Element of {1,2,3} holds b1 . (x,y) = x example32"/\" y ) & ( for x, y being Element of {1,2,3} holds b2 . (x,y) = x example32"/\" y ) holds
b1 = b2
proof end;
end;

:: deftheorem Defx7 defines example32\/ LATTAD_1:def 17 :
for b1 being BinOp of {1,2,3} holds
( b1 = example32\/ iff for x, y being Element of {1,2,3} holds b1 . (x,y) = x example32"\/" y );

:: deftheorem Defx8 defines example32/\ LATTAD_1:def 18 :
for b1 being BinOp of {1,2,3} holds
( b1 = example32/\ iff for x, y being Element of {1,2,3} holds b1 . (x,y) = x example32"/\" y );

theorem :: LATTAD_1:65
ex L being non empty LattStr st
( ( for x being Element of L holds
( x = 1 or x = 2 or x = 3 ) ) & ( for x, y being Element of L holds
( ( not x "/\" y = 1 or y = 1 or ( y = 2 & ( x = 1 or x = 3 ) ) ) & ( ( y = 1 or ( y = 2 & ( x = 1 or x = 3 ) ) ) implies x "/\" y = 1 ) & ( x "/\" y = 2 implies ( x = 2 & y = 2 ) ) & ( x = 2 & y = 2 implies x "/\" y = 2 ) & ( x "/\" y = 3 implies y = 3 ) & ( y = 3 implies x "/\" y = 3 ) ) ) & ( for x, y being Element of L holds
( ( x "\/" y = 1 implies ( x = 1 & ( y = 1 or y = 3 ) ) ) & ( x = 1 & ( y = 1 or y = 3 ) implies x "\/" y = 1 ) & ( not x "\/" y = 2 or x = 2 or ( x = 1 & y = 2 ) ) & ( ( x = 2 or ( x = 1 & y = 2 ) ) implies x "\/" y = 2 ) & ( x "\/" y = 3 implies x = 3 ) & ( x = 3 implies x "\/" y = 3 ) ) ) & L is GAD_Lattice & L is not AD_Lattice )
proof end;

Lmx3: ex x being Element of {1,2,3} st x = 2
proof end;

definition
let x, y be Element of {1,2,3};
func x example33"/\" y -> Element of {1,2,3} equals :Defx5: :: LATTAD_1:def 19
1 if ( x = 1 & y = 1 )
2 if ( y = 2 or ( y = 1 & ( x = 2 or x = 3 ) ) )
3 if y = 3
;
coherence
( ( x = 1 & y = 1 implies 1 is Element of {1,2,3} ) & ( ( y = 2 or ( y = 1 & ( x = 2 or x = 3 ) ) ) implies 2 is Element of {1,2,3} ) & ( y = 3 implies 3 is Element of {1,2,3} ) )
by Lmx3;
consistency
for b1 being Element of {1,2,3} holds
( ( x = 1 & y = 1 & ( y = 2 or ( y = 1 & ( x = 2 or x = 3 ) ) ) implies ( b1 = 1 iff b1 = 2 ) ) & ( x = 1 & y = 1 & y = 3 implies ( b1 = 1 iff b1 = 3 ) ) & ( ( y = 2 or ( y = 1 & ( x = 2 or x = 3 ) ) ) & y = 3 implies ( b1 = 2 iff b1 = 3 ) ) )
;
func x example33"\/" y -> Element of {1,2,3} equals :Defx6: :: LATTAD_1:def 20
1 if ( x = 1 or ( x = 2 & y = 1 ) )
2 if ( x = 2 & ( y = 2 or y = 3 ) )
3 if x = 3
;
coherence
( ( ( x = 1 or ( x = 2 & y = 1 ) ) implies 1 is Element of {1,2,3} ) & ( x = 2 & ( y = 2 or y = 3 ) implies 2 is Element of {1,2,3} ) & ( x = 3 implies 3 is Element of {1,2,3} ) )
;
consistency
for b1 being Element of {1,2,3} holds
( ( ( x = 1 or ( x = 2 & y = 1 ) ) & x = 2 & ( y = 2 or y = 3 ) implies ( b1 = 1 iff b1 = 2 ) ) & ( ( x = 1 or ( x = 2 & y = 1 ) ) & x = 3 implies ( b1 = 1 iff b1 = 3 ) ) & ( x = 2 & ( y = 2 or y = 3 ) & x = 3 implies ( b1 = 2 iff b1 = 3 ) ) )
;
end;

:: deftheorem Defx5 defines example33"/\" LATTAD_1:def 19 :
for x, y being Element of {1,2,3} holds
( ( x = 1 & y = 1 implies x example33"/\" y = 1 ) & ( ( y = 2 or ( y = 1 & ( x = 2 or x = 3 ) ) ) implies x example33"/\" y = 2 ) & ( y = 3 implies x example33"/\" y = 3 ) );

:: deftheorem Defx6 defines example33"\/" LATTAD_1:def 20 :
for x, y being Element of {1,2,3} holds
( ( ( x = 1 or ( x = 2 & y = 1 ) ) implies x example33"\/" y = 1 ) & ( x = 2 & ( y = 2 or y = 3 ) implies x example33"\/" y = 2 ) & ( x = 3 implies x example33"\/" y = 3 ) );

definition
func example33\/ -> BinOp of {1,2,3} means :Defx7: :: LATTAD_1:def 21
for x, y being Element of {1,2,3} holds it . (x,y) = x example33"\/" y;
existence
ex b1 being BinOp of {1,2,3} st
for x, y being Element of {1,2,3} holds b1 . (x,y) = x example33"\/" y
proof end;
uniqueness
for b1, b2 being BinOp of {1,2,3} st ( for x, y being Element of {1,2,3} holds b1 . (x,y) = x example33"\/" y ) & ( for x, y being Element of {1,2,3} holds b2 . (x,y) = x example33"\/" y ) holds
b1 = b2
proof end;
func example33/\ -> BinOp of {1,2,3} means :Defx8: :: LATTAD_1:def 22
for x, y being Element of {1,2,3} holds it . (x,y) = x example33"/\" y;
existence
ex b1 being BinOp of {1,2,3} st
for x, y being Element of {1,2,3} holds b1 . (x,y) = x example33"/\" y
proof end;
uniqueness
for b1, b2 being BinOp of {1,2,3} st ( for x, y being Element of {1,2,3} holds b1 . (x,y) = x example33"/\" y ) & ( for x, y being Element of {1,2,3} holds b2 . (x,y) = x example33"/\" y ) holds
b1 = b2
proof end;
end;

:: deftheorem Defx7 defines example33\/ LATTAD_1:def 21 :
for b1 being BinOp of {1,2,3} holds
( b1 = example33\/ iff for x, y being Element of {1,2,3} holds b1 . (x,y) = x example33"\/" y );

:: deftheorem Defx8 defines example33/\ LATTAD_1:def 22 :
for b1 being BinOp of {1,2,3} holds
( b1 = example33/\ iff for x, y being Element of {1,2,3} holds b1 . (x,y) = x example33"/\" y );

theorem :: LATTAD_1:66
ex L being non empty LattStr st
( ( for x being Element of L holds
( x = 1 or x = 2 or x = 3 ) ) & ( for x, y being Element of L holds
( ( x "/\" y = 1 implies ( x = 1 & y = 1 ) ) & ( x = 1 & y = 1 implies x "/\" y = 1 ) & ( not x "/\" y = 2 or y = 2 or ( y = 1 & ( x = 2 or x = 3 ) ) ) & ( ( y = 2 or ( y = 1 & ( x = 2 or x = 3 ) ) ) implies x "/\" y = 2 ) & ( x "/\" y = 3 implies y = 3 ) & ( y = 3 implies x "/\" y = 3 ) ) ) & ( for x, y being Element of L holds
( ( not x "\/" y = 1 or x = 1 or ( x = 2 & y = 1 ) ) & ( ( x = 1 or ( x = 2 & y = 1 ) ) implies x "\/" y = 1 ) & ( x "\/" y = 2 implies ( x = 2 & ( y = 2 or y = 3 ) ) ) & ( x = 2 & ( y = 2 or y = 3 ) implies x "\/" y = 2 ) & ( x "\/" y = 3 implies x = 3 ) & ( x = 3 implies x "\/" y = 3 ) ) ) & L is GAD_Lattice )
proof end;

:: like NAT_LAT ::
definition
let L be non empty LattStr ;
mode SubLattStr of L -> LattStr means :Defx1: :: LATTAD_1:def 23
( the carrier of it c= the carrier of L & the L_join of it = the L_join of L || the carrier of it & the L_meet of it = the L_meet of L || the carrier of it );
existence
ex b1 being LattStr st
( the carrier of b1 c= the carrier of L & the L_join of b1 = the L_join of L || the carrier of b1 & the L_meet of b1 = the L_meet of L || the carrier of b1 )
proof end;
end;

:: deftheorem Defx1 defines SubLattStr LATTAD_1:def 23 :
for L being non empty LattStr
for b2 being LattStr holds
( b2 is SubLattStr of L iff ( the carrier of b2 c= the carrier of L & the L_join of b2 = the L_join of L || the carrier of b2 & the L_meet of b2 = the L_meet of L || the carrier of b2 ) );

registration
let L be non empty LattStr ;
cluster strict for SubLattStr of L;
correctness
existence
ex b1 being SubLattStr of L st b1 is strict
;
proof end;
end;

definition
end;

:: deftheorem LATTAD_1:def 24 :
canceled;

:: deftheorem LATTAD_1:def 25 :
canceled;

registration
let L be non empty LattStr ;
cluster non empty meet-closed join-closed for Element of bool the carrier of L;
existence
ex b1 being Subset of L st
( b1 is meet-closed & b1 is join-closed & not b1 is empty )
proof end;
end;

definition
let L be non empty LattStr ;
mode ClosedSubset of L is meet-closed join-closed Subset of L;
end;

definition
let L be non empty LattStr ;
let P be ClosedSubset of L;
func latt (L,P) -> strict SubLattStr of L means :Defx4: :: LATTAD_1:def 26
the carrier of it = P;
existence
ex b1 being strict SubLattStr of L st the carrier of b1 = P
proof end;
uniqueness
for b1, b2 being strict SubLattStr of L st the carrier of b1 = P & the carrier of b2 = P holds
b1 = b2
proof end;
end;

:: deftheorem Defx4 defines latt LATTAD_1:def 26 :
for L being non empty LattStr
for P being ClosedSubset of L
for b3 being strict SubLattStr of L holds
( b3 = latt (L,P) iff the carrier of b3 = P );

registration
let L be non empty LattStr ;
let S be non empty ClosedSubset of L;
cluster latt (L,S) -> non empty strict ;
correctness
coherence
not latt (L,S) is empty
;
by Defx4;
end;

registration
let L be non empty LattStr ;
cluster non empty for SubLattStr of L;
correctness
existence
not for b1 being SubLattStr of L holds b1 is empty
;
proof end;
end;

theorem Thx3: :: LATTAD_1:67
for L being non empty LattStr
for S being non empty SubLattStr of L
for x1, x2 being Element of L
for y1, y2 being Element of S st x1 = y1 & x2 = y2 holds
x1 "\/" x2 = y1 "\/" y2
proof end;

theorem Thx4: :: LATTAD_1:68
for L being non empty LattStr
for S being non empty SubLattStr of L
for x1, x2 being Element of L
for y1, y2 being Element of S st x1 = y1 & x2 = y2 holds
x1 "/\" x2 = y1 "/\" y2
proof end;

theorem Thx1: :: LATTAD_1:69
for L being non empty LattStr
for S being non empty ClosedSubset of L holds
( ( L is meet-associative implies latt (L,S) is meet-associative ) & ( L is meet-absorbing implies latt (L,S) is meet-absorbing ) & ( L is meet-commutative implies latt (L,S) is meet-commutative ) & ( L is join-associative implies latt (L,S) is join-associative ) & ( L is join-absorbing implies latt (L,S) is join-absorbing ) & ( L is join-commutative implies latt (L,S) is join-commutative ) & ( L is Meet-Absorbing implies latt (L,S) is Meet-Absorbing ) & ( L is distributive implies latt (L,S) is distributive ) & ( L is left-Distributive implies latt (L,S) is left-Distributive ) )
proof end;

theorem :: LATTAD_1:70
for L being with_zero GAD_Lattice
for a being Element of L
for X being set st X = { (x "/\" a) where x is Element of L : verum } holds
( X = { x where x is Element of L : x [= a } & X is ClosedSubset of L )
proof end;

theorem :: LATTAD_1:71
for L being with_zero GAD_Lattice
for a being Element of L
for S being non empty ClosedSubset of L
for b being Element of (latt (L,S)) st b = a & S = { (x "/\" a) where x is Element of L : verum } holds
( latt (L,S) is Lattice-like & latt (L,S) is distributive & ( for c being Element of (latt (L,S)) holds
( b "\/" c = b & c "\/" b = b & c [= b ) ) )
proof end;