:: 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 b₁ being non empty LattStr st b₁ is trivial holds
b₁ 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 b₁ being non empty LattStr st b₁ is trivial holds
( b₁ is Distributive & b₁ is Meet-absorbing & b₁ is Meet-Absorbing & b₁ is meet-Absorbing ) ;

cluster non empty trivial -> non empty Lattice-like for LattStr ;

coherence
for b₁ being non empty LattStr st b₁ is trivial holds
b₁ 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 b₁ being Lattice st b₁ is trivial

proof end;

end;

registration

cluster non empty distributive meet-Absorbing Distributive Meet-absorbing Meet-Absorbing for LattStr ;

existence
ex b₁ being non empty LattStr st
( b₁ is Distributive & b₁ is distributive & b₁ is Meet-absorbing & b₁ is Meet-Absorbing & b₁ 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 b₁ being non empty LattStr st b₁ is trivial holds
( b₁ is meet-associative & b₁ is distributive & b₁ is left-Distributive & b₁ is Meet-Absorbing ) ;

end;

registration

cluster non empty meet-associative meet-absorbing join-absorbing distributive Meet-Absorbing left-Distributive for LattStr ;

existence
ex b₁ being non empty LattStr st
( b₁ is meet-associative & b₁ is distributive & b₁ is left-Distributive & b₁ is join-absorbing & b₁ is Meet-Absorbing & b₁ 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 b₁ being Relation of the carrier of L st b₁ = LatOrder L holds
b₁ 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 b₁ being Relation of the carrier of L st b₁ = ThetaOrder L holds
b₁ 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 b₁ being Element of L st
( a [= b₁ & b [= b₁ & ( for x being Element of L st a [= x & b [= x holds
b₁ [= x ) ) by A1;
correctness
uniqueness
for b₁, b₂ being Element of L st a [= b₁ & b [= b₁ & ( for x being Element of L st a [= x & b [= x holds
b₁ [= x ) & a [= b₂ & b [= b₂ & ( for x being Element of L st a [= x & b [= x holds
b₂ [= x ) holds
b₁ = b₂;

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 b₄ being Element of L holds
( b₄ = lub (a,b) iff ( a [= b₄ & b [= b₄ & ( for x being Element of L st a [= x & b [= x holds
b₄ [= 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 b₁ being Element of L st
( b₁ [= a & b₁ [= b & ( for x being Element of L st x [= a & x [= b holds
x [= b₁ ) ) by A1;
correctness
uniqueness
for b₁, b₂ being Element of L st b₁ [= a & b₁ [= b & ( for x being Element of L st x [= a & x [= b holds
x [= b₁ ) & b₂ [= a & b₂ [= b & ( for x being Element of L st x [= a & x [= b holds
x [= b₂ ) holds
b₁ = b₂;

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 b₄ being Element of L holds
( b₄ = glb (a,b) iff ( b₄ [= a & b₄ [= b & ( for x being Element of L st x [= a & x [= b holds
x [= b₄ ) ) );

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 b₁ being GAD_Lattice st b₁ is join-commutative holds
b₁ 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 b₁ being GAD_Lattice st b₁ is ADL-absorbing holds
b₁ 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 b₁ being GAD_Lattice st b₁ is join-commutative holds
b₁ 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 b₁ being GAD_Lattice st b₁ is meet-commutative holds
b₁ 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 b₁ being GAD_Lattice st b₁ is trivial holds
b₁ 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 b₁ being GAD_Lattice st b₁ 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 b₁ being Element of L st
for a being Element of L holds b₁ "/\" a = b₁ by A1;
uniqueness
for b₁, b₂ being Element of L st ( for a being Element of L holds b₁ "/\" a = b₁ ) & ( for a being Element of L holds b₂ "/\" a = b₂ ) holds
b₁ = b₂

proof end;

end;

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

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 b₁ being Element of {1,2,3} holds
( ( ( y = 1 or ( y = 2 & ( x = 1 or x = 3 ) ) ) & x = 2 & y = 2 implies ( b₁ = 1 iff b₁ = 2 ) ) & ( ( y = 1 or ( y = 2 & ( x = 1 or x = 3 ) ) ) & y = 3 implies ( b₁ = 1 iff b₁ = 3 ) ) & ( x = 2 & y = 2 & y = 3 implies ( b₁ = 2 iff b₁ = 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 b₁ being Element of {1,2,3} holds
( ( x = 1 & ( y = 1 or y = 3 ) & ( x = 2 or ( x = 1 & y = 2 ) ) implies ( b₁ = 1 iff b₁ = 2 ) ) & ( x = 1 & ( y = 1 or y = 3 ) & x = 3 implies ( b₁ = 1 iff b₁ = 3 ) ) & ( ( x = 2 or ( x = 1 & y = 2 ) ) & x = 3 implies ( b₁ = 2 iff b₁ = 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 b₁ being BinOp of {1,2,3} st
for x, y being Element of {1,2,3} holds b₁ . (x,y) = x example32"\/" y

proof end;

uniqueness
for b₁, b₂ being BinOp of {1,2,3} st ( for x, y being Element of {1,2,3} holds b₁ . (x,y) = x example32"\/" y ) & ( for x, y being Element of {1,2,3} holds b₂ . (x,y) = x example32"\/" y ) holds
b₁ = b₂

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 b₁ being BinOp of {1,2,3} st
for x, y being Element of {1,2,3} holds b₁ . (x,y) = x example32"/\" y

proof end;

uniqueness
for b₁, b₂ being BinOp of {1,2,3} st ( for x, y being Element of {1,2,3} holds b₁ . (x,y) = x example32"/\" y ) & ( for x, y being Element of {1,2,3} holds b₂ . (x,y) = x example32"/\" y ) holds
b₁ = b₂

proof end;

end;

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

:: deftheorem Defx8 defines example32/\ LATTAD_1:def 18 :
for b₁ being BinOp of {1,2,3} holds
( b₁ = example32/\ iff for x, y being Element of {1,2,3} holds b₁ . (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 b₁ being Element of {1,2,3} holds
( ( x = 1 & y = 1 & ( y = 2 or ( y = 1 & ( x = 2 or x = 3 ) ) ) implies ( b₁ = 1 iff b₁ = 2 ) ) & ( x = 1 & y = 1 & y = 3 implies ( b₁ = 1 iff b₁ = 3 ) ) & ( ( y = 2 or ( y = 1 & ( x = 2 or x = 3 ) ) ) & y = 3 implies ( b₁ = 2 iff b₁ = 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 b₁ being Element of {1,2,3} holds
( ( ( x = 1 or ( x = 2 & y = 1 ) ) & x = 2 & ( y = 2 or y = 3 ) implies ( b₁ = 1 iff b₁ = 2 ) ) & ( ( x = 1 or ( x = 2 & y = 1 ) ) & x = 3 implies ( b₁ = 1 iff b₁ = 3 ) ) & ( x = 2 & ( y = 2 or y = 3 ) & x = 3 implies ( b₁ = 2 iff b₁ = 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 b₁ being BinOp of {1,2,3} st
for x, y being Element of {1,2,3} holds b₁ . (x,y) = x example33"\/" y

proof end;

uniqueness
for b₁, b₂ being BinOp of {1,2,3} st ( for x, y being Element of {1,2,3} holds b₁ . (x,y) = x example33"\/" y ) & ( for x, y being Element of {1,2,3} holds b₂ . (x,y) = x example33"\/" y ) holds
b₁ = b₂

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 b₁ being BinOp of {1,2,3} st
for x, y being Element of {1,2,3} holds b₁ . (x,y) = x example33"/\" y

proof end;

uniqueness
for b₁, b₂ being BinOp of {1,2,3} st ( for x, y being Element of {1,2,3} holds b₁ . (x,y) = x example33"/\" y ) & ( for x, y being Element of {1,2,3} holds b₂ . (x,y) = x example33"/\" y ) holds
b₁ = b₂

proof end;

end;

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

:: deftheorem Defx8 defines example33/\ LATTAD_1:def 22 :
for b₁ being BinOp of {1,2,3} holds
( b₁ = example33/\ iff for x, y being Element of {1,2,3} holds b₁ . (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 b₁ being LattStr st
( the carrier of b₁ c= the carrier of L & the L_join of b₁ = the L_join of L || the carrier of b₁ & the L_meet of b₁ = the L_meet of L || the carrier of b₁ )

proof end;

end;

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

registration

let L be non empty LattStr ;

cluster strict for SubLattStr of L;

correctness
existence
ex b₁ being SubLattStr of L st b₁ 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 b₁ being Subset of L st
( b₁ is meet-closed & b₁ is join-closed & not b₁ 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 b₁ being strict SubLattStr of L st the carrier of b₁ = P

proof end;

uniqueness
for b₁, b₂ being strict SubLattStr of L st the carrier of b₁ = P & the carrier of b₂ = P holds
b₁ = b₂

proof end;

end;

:: deftheorem Defx4 defines latt LATTAD_1:def 26 :
for L being non empty LattStr
for P being ClosedSubset of L
for b₃ being strict SubLattStr of L holds
( b₃ = latt (L,P) iff the carrier of b₃ = 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 b₁ being SubLattStr of L holds b₁ 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;