:: by Adam Grabowski

::

:: Received September 26, 2014

:: Copyright (c) 2014-2019 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 )

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

definition

let L be non empty LattStr ;

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)

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

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;

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;

for x, y being Element of L holds (x "\/" y) "/\" x = x;

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

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

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

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

for b_{1} being non empty LattStr st b_{1} is trivial holds

( b_{1} is Distributive & b_{1} is Meet-absorbing & b_{1} is Meet-Absorbing & b_{1} is meet-Absorbing )
;

coherence

for b_{1} being non empty LattStr st b_{1} is trivial holds

b_{1} is Lattice-like
end;

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

coherence for b

( b

coherence

for b

b

proof end;

registration

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

cluster non empty trivial join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like join-Associative meet-Associative meet-Absorbing for LattStr ;

existence ex b

proof end;

registration

ex b_{1} being non empty LattStr st

( b_{1} is Distributive & b_{1} is distributive & b_{1} is Meet-absorbing & b_{1} is Meet-Absorbing & b_{1} is meet-Absorbing )
end;

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

existence ex b

( b

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

for x, y being Element of L holds

( x "\/" y = x iff x "/\" y = y ) by DefA1, ROBBINS3:def 3;

theorem :: LATTAD_1:10

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 )

for x, y being Element of L holds

( (x "/\" y) "\/" x = x iff x "/\" (y "\/" x) = x )

proof end;

theorem :: LATTAD_1:13

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

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

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

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;

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

::

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

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)

::

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

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;

for x, y being Element of L holds x "/\" (y "\/" x) = x;

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

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

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

for b_{1} being non empty LattStr st b_{1} is trivial holds

( b_{1} is meet-associative & b_{1} is distributive & b_{1} is left-Distributive & b_{1} is Meet-Absorbing )
;

end;

cluster non empty trivial -> non empty meet-associative distributive Meet-Absorbing left-Distributive for LattStr ;

coherence for b

( b

registration

ex b_{1} being non empty LattStr st

( b_{1} is meet-associative & b_{1} is distributive & b_{1} is left-Distributive & b_{1} is join-absorbing & b_{1} is Meet-Absorbing & b_{1} is meet-absorbing )
end;

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

existence ex b

( b

proof end;

definition

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

end;
theorem :: LATTAD_1:22

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;

for x, y being Element of L holds

( x "\/" y = y iff x "/\" y = x ) by LATTICES:def 9, LATTICES:def 8;

definition

let L be non empty LattStr ;

{ [a,b] where a, b is Element of L : a [= b } is Relation

end;
::: 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 } ;

{ [a,b] where a, b is Element of L : a [= b } is Relation

proof 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 } ;

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 )

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

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

registration

let L be GAD_Lattice;

correctness

coherence

for b_{1} being Relation of the carrier of L st b_{1} = LatOrder L holds

b_{1} is total ;

end;
correctness

coherence

for b

b

proof end;

definition

let L be non empty LattStr ;

{ [a,b] where a, b is Element of L : a "/\" b = b } is Relation

end;
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 } ;

{ [a,b] where a, b is Element of L : a "/\" b = b } is Relation

proof 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 } ;

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 )

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

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

registration

let L be GAD_Lattice;

correctness

coherence

for b_{1} being Relation of the carrier of L st b_{1} = ThetaOrder L holds

b_{1} is total ;

end;
correctness

coherence

for b

b

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

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;

coherence

LatOrder L is reflexive

LatOrder L is transitive

end;
coherence

LatOrder L is reflexive

proof end;

coherence LatOrder L is transitive

proof end;

registration

let L be GAD_Lattice;

coherence

ThetaOrder L is reflexive

ThetaOrder L is transitive

end;
coherence

ThetaOrder L is reflexive

proof end;

coherence ThetaOrder L is transitive

proof end;

theorem :: LATTAD_1:32

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;

end;
let a, b be Element of L;

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

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

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 ;

ex b_{1} being Element of L st

( a [= b_{1} & b [= b_{1} & ( for x being Element of L st a [= x & b [= x holds

b_{1} [= x ) )
by A1;

correctness

uniqueness

for b_{1}, b_{2} being Element of L st a [= b_{1} & b [= b_{1} & ( for x being Element of L st a [= x & b [= x holds

b_{1} [= x ) & a [= b_{2} & b [= b_{2} & ( for x being Element of L st a [= x & b [= x holds

b_{2} [= x ) holds

b_{1} = b_{2};

end;
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 ( a [= it & b [= it & ( for x being Element of L st a [= x & b [= x holds

it [= x ) );

ex b

( a [= b

b

correctness

uniqueness

for b

b

b

b

proof 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_{4} being Element of L holds

( b_{4} = lub (a,b) iff ( a [= b_{4} & b [= b_{4} & ( for x being Element of L st a [= x & b [= x holds

b_{4} [= x ) ) );

for L being GAD_Lattice

for a, b being Element of L st ex_lub_of a,b holds

for b

( b

b

definition

let L be GAD_Lattice;

let a, b be Element of L;

assume A1: ex_glb_of a,b ;

ex b_{1} being Element of L st

( b_{1} [= a & b_{1} [= b & ( for x being Element of L st x [= a & x [= b holds

x [= b_{1} ) )
by A1;

correctness

uniqueness

for b_{1}, b_{2} being Element of L st b_{1} [= a & b_{1} [= b & ( for x being Element of L st x [= a & x [= b holds

x [= b_{1} ) & b_{2} [= a & b_{2} [= b & ( for x being Element of L st x [= a & x [= b holds

x [= b_{2} ) holds

b_{1} = b_{2};

end;
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 ( it [= a & it [= b & ( for x being Element of L st x [= a & x [= b holds

x [= it ) );

ex b

( b

x [= b

correctness

uniqueness

for b

x [= b

x [= b

b

proof 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_{4} being Element of L holds

( b_{4} = glb (a,b) iff ( b_{4} [= a & b_{4} [= b & ( for x being Element of L st x [= a & x [= b holds

x [= b_{4} ) ) );

for L being GAD_Lattice

for a, b being Element of L st ex_glb_of a,b holds

for b

( b

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

theorem :: LATTAD_1:34

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 )

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;

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 )

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;

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:40

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

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

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

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

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

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

S1:
( ex_lub_of a,b & a "\/" b = lub (a,b) )
by Z1;
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;
x "\/" y = y "\/" x by ZZ;

hence ( ex_lub_of x,y & x "\/" y = lub (x,y) ) by Th381i4; :: thesis: verum

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

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

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;

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

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;

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

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;

definition

let L be GAD_Lattice;

RelStr(# the carrier of L,(LatOrder L) #) is strict RelStr ;

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

RelStr(# the carrier of L,(LatOrder L) #) is strict RelStr ;

:: deftheorem defines LatRelStr LATTAD_1:def 12 :

for L being GAD_Lattice holds LatRelStr L = RelStr(# the carrier of L,(LatOrder L) #);

for L being GAD_Lattice holds LatRelStr L = RelStr(# the carrier of L,(LatOrder L) #);

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

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

( L is join-commutative iff ( L is Lattice-like & L is distributive ) )

proof end;

theorem :: LATTAD_1:54

registration
end;

registration

for b_{1} being GAD_Lattice st b_{1} is join-commutative holds

b_{1} is ADL-absorbing
by Th31143;

for b_{1} being GAD_Lattice st b_{1} is ADL-absorbing holds

b_{1} is join-commutative
by Th31143;

end;

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

coherence for b

b

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

coherence for b

b

registration

for b_{1} being GAD_Lattice st b_{1} is join-commutative holds

b_{1} is meet-commutative
by Th31145;

for b_{1} being GAD_Lattice st b_{1} is meet-commutative holds

b_{1} is join-commutative
by Th31145;

end;

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

coherence for b

b

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

coherence for b

b

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

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

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

for a, b, c being Element of L holds (a "\/" b) "/\" c = (b "\/" a) "/\" c

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

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

for b_{1} being GAD_Lattice st b_{1} is trivial holds

b_{1} is with_zero
end;

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

coherence for b

b

proof end;

registration

ex b_{1} being GAD_Lattice st b_{1} is with_zero
end;

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

existence ex b

proof end;

definition

let L be GAD_Lattice;

assume A1: L is with_zero ;

ex b_{1} being Element of L st

for a being Element of L holds b_{1} "/\" a = b_{1}
by A1;

uniqueness

for b_{1}, b_{2} being Element of L st ( for a being Element of L holds b_{1} "/\" a = b_{1} ) & ( for a being Element of L holds b_{2} "/\" a = b_{2} ) holds

b_{1} = b_{2}

end;
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 for a being Element of L holds it "/\" a = it;

ex b

for a being Element of L holds b

uniqueness

for b

b

proof end;

:: deftheorem GADL0 defines bottom LATTAD_1:def 14 :

for L being GAD_Lattice st L is with_zero holds

for b_{2} being Element of L holds

( b_{2} = bottom L iff for a being Element of L holds b_{2} "/\" a = b_{2} );

for L being GAD_Lattice st L is with_zero holds

for b

( b

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 )

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

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

( ( ( 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_{1} being Element of {1,2,3} holds

( ( ( y = 1 or ( y = 2 & ( x = 1 or x = 3 ) ) ) & x = 2 & y = 2 implies ( b_{1} = 1 iff b_{1} = 2 ) ) & ( ( y = 1 or ( y = 2 & ( x = 1 or x = 3 ) ) ) & y = 3 implies ( b_{1} = 1 iff b_{1} = 3 ) ) & ( x = 2 & y = 2 & y = 3 implies ( b_{1} = 2 iff b_{1} = 3 ) ) )
;

( ( 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_{1} being Element of {1,2,3} holds

( ( x = 1 & ( y = 1 or y = 3 ) & ( x = 2 or ( x = 1 & y = 2 ) ) implies ( b_{1} = 1 iff b_{1} = 2 ) ) & ( x = 1 & ( y = 1 or y = 3 ) & x = 3 implies ( b_{1} = 1 iff b_{1} = 3 ) ) & ( ( x = 2 or ( x = 1 & y = 2 ) ) & x = 3 implies ( b_{1} = 2 iff b_{1} = 3 ) ) )
;

end;
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 1 if ( y = 1 or ( y = 2 & ( x = 1 or x = 3 ) ) )

2 if ( x = 2 & y = 2 )

3 if y = 3

;

( ( ( 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

( ( ( y = 1 or ( y = 2 & ( x = 1 or x = 3 ) ) ) & x = 2 & y = 2 implies ( b

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 1 if ( x = 1 & ( y = 1 or y = 3 ) )

2 if ( x = 2 or ( x = 1 & y = 2 ) )

3 if x = 3

;

( ( 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

( ( x = 1 & ( y = 1 or y = 3 ) & ( x = 2 or ( x = 1 & y = 2 ) ) implies ( b

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

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

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

ex b_{1} being BinOp of {1,2,3} st

for x, y being Element of {1,2,3} holds b_{1} . (x,y) = x example32"\/" y

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

b_{1} = b_{2}

ex b_{1} being BinOp of {1,2,3} st

for x, y being Element of {1,2,3} holds b_{1} . (x,y) = x example32"/\" y

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

b_{1} = b_{2}
end;

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

ex b

for x, y being Element of {1,2,3} holds b

proof end;

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

ex b

for x, y being Element of {1,2,3} holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Defx7 defines example32\/ LATTAD_1:def 17 :

for b_{1} being BinOp of {1,2,3} holds

( b_{1} = example32\/ iff for x, y being Element of {1,2,3} holds b_{1} . (x,y) = x example32"\/" y );

for b

( b

:: deftheorem Defx8 defines example32/\ LATTAD_1:def 18 :

for b_{1} being BinOp of {1,2,3} holds

( b_{1} = example32/\ iff for x, y being Element of {1,2,3} holds b_{1} . (x,y) = x example32"/\" y );

for b

( b

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 )

( ( 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};

( ( 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_{1} being Element of {1,2,3} holds

( ( x = 1 & y = 1 & ( y = 2 or ( y = 1 & ( x = 2 or x = 3 ) ) ) implies ( b_{1} = 1 iff b_{1} = 2 ) ) & ( x = 1 & y = 1 & y = 3 implies ( b_{1} = 1 iff b_{1} = 3 ) ) & ( ( y = 2 or ( y = 1 & ( x = 2 or x = 3 ) ) ) & y = 3 implies ( b_{1} = 2 iff b_{1} = 3 ) ) )
;

( ( ( 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_{1} being Element of {1,2,3} holds

( ( ( x = 1 or ( x = 2 & y = 1 ) ) & x = 2 & ( y = 2 or y = 3 ) implies ( b_{1} = 1 iff b_{1} = 2 ) ) & ( ( x = 1 or ( x = 2 & y = 1 ) ) & x = 3 implies ( b_{1} = 1 iff b_{1} = 3 ) ) & ( x = 2 & ( y = 2 or y = 3 ) & x = 3 implies ( b_{1} = 2 iff b_{1} = 3 ) ) )
;

end;
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 1 if ( x = 1 & y = 1 )

2 if ( y = 2 or ( y = 1 & ( x = 2 or x = 3 ) ) )

3 if y = 3

;

( ( 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

( ( x = 1 & y = 1 & ( y = 2 or ( y = 1 & ( x = 2 or x = 3 ) ) ) implies ( b

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 1 if ( x = 1 or ( x = 2 & y = 1 ) )

2 if ( x = 2 & ( y = 2 or y = 3 ) )

3 if x = 3

;

( ( ( 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

( ( ( x = 1 or ( x = 2 & y = 1 ) ) & x = 2 & ( y = 2 or y = 3 ) implies ( b

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

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

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

ex b_{1} being BinOp of {1,2,3} st

for x, y being Element of {1,2,3} holds b_{1} . (x,y) = x example33"\/" y

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

b_{1} = b_{2}

ex b_{1} being BinOp of {1,2,3} st

for x, y being Element of {1,2,3} holds b_{1} . (x,y) = x example33"/\" y

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

b_{1} = b_{2}
end;

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

ex b

for x, y being Element of {1,2,3} holds b

proof end;

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

ex b

for x, y being Element of {1,2,3} holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Defx7 defines example33\/ LATTAD_1:def 21 :

for b_{1} being BinOp of {1,2,3} holds

( b_{1} = example33\/ iff for x, y being Element of {1,2,3} holds b_{1} . (x,y) = x example33"\/" y );

for b

( b

:: deftheorem Defx8 defines example33/\ LATTAD_1:def 22 :

for b_{1} being BinOp of {1,2,3} holds

( b_{1} = example33/\ iff for x, y being Element of {1,2,3} holds b_{1} . (x,y) = x example33"/\" y );

for b

( b

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 )

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

ex b_{1} being LattStr st

( the carrier of b_{1} c= the carrier of L & the L_join of b_{1} = the L_join of L || the carrier of b_{1} & the L_meet of b_{1} = the L_meet of L || the carrier of b_{1} )

end;
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 ( 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 );

ex b

( the carrier of b

proof end;

:: deftheorem Defx1 defines SubLattStr LATTAD_1:def 23 :

for L being non empty LattStr

for b_{2} being LattStr holds

( b_{2} is SubLattStr of L iff ( the carrier of b_{2} c= the carrier of L & the L_join of b_{2} = the L_join of L || the carrier of b_{2} & the L_meet of b_{2} = the L_meet of L || the carrier of b_{2} ) );

for L being non empty LattStr

for b

( b

registration

let L be non empty LattStr ;

correctness

existence

ex b_{1} being SubLattStr of L st b_{1} is strict ;

end;
correctness

existence

ex b

proof end;

:: like LATTICES ::

definition

let L be non empty LattStr ;

let S be Subset of L;

end;
let S be Subset of L;

attr S is meet-closed means :Defx2: :: LATTAD_1:def 24

for p, q being Element of L st p in S & q in S holds

p "/\" q in S;

for p, q being Element of L st p in S & q in S holds

p "/\" q in S;

attr S is join-closed means :Defx3: :: LATTAD_1:def 25

for p, q being Element of L st p in S & q in S holds

p "\/" q in S;

for p, q being Element of L st p in S & q in S holds

p "\/" q in S;

:: deftheorem Defx2 defines meet-closed LATTAD_1:def 24 :

for L being non empty LattStr

for S being Subset of L holds

( S is meet-closed iff for p, q being Element of L st p in S & q in S holds

p "/\" q in S );

for L being non empty LattStr

for S being Subset of L holds

( S is meet-closed iff for p, q being Element of L st p in S & q in S holds

p "/\" q in S );

:: deftheorem Defx3 defines join-closed LATTAD_1:def 25 :

for L being non empty LattStr

for S being Subset of L holds

( S is join-closed iff for p, q being Element of L st p in S & q in S holds

p "\/" q in S );

for L being non empty LattStr

for S being Subset of L holds

( S is join-closed iff for p, q being Element of L st p in S & q in S holds

p "\/" q in S );

registration

let L be non empty LattStr ;

existence

ex b_{1} being Subset of L st

( b_{1} is meet-closed & b_{1} is join-closed & not b_{1} is empty )

end;
existence

ex b

( b

proof end;

definition
end;

definition

let L be non empty LattStr ;

let P be ClosedSubset of L;

existence

ex b_{1} being strict SubLattStr of L st the carrier of b_{1} = P

for b_{1}, b_{2} being strict SubLattStr of L st the carrier of b_{1} = P & the carrier of b_{2} = P holds

b_{1} = b_{2}

end;
let P be ClosedSubset of L;

existence

ex b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Defx4 defines latt LATTAD_1:def 26 :

for L being non empty LattStr

for P being ClosedSubset of L

for b_{3} being strict SubLattStr of L holds

( b_{3} = latt (L,P) iff the carrier of b_{3} = P );

for L being non empty LattStr

for P being ClosedSubset of L

for b

( b

registration

let L be non empty LattStr ;

let S be non empty ClosedSubset of L;

correctness

coherence

not latt (L,S) is empty ;

by Defx4;

end;
let S be non empty ClosedSubset of L;

correctness

coherence

not latt (L,S) is empty ;

by Defx4;

registration

let L be non empty LattStr ;

correctness

existence

not for b_{1} being SubLattStr of L holds b_{1} is empty ;

end;
correctness

existence

not for b

proof 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

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

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

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 )

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

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;

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