:: NAT_LAT semantic presentation
begin
definition
func hcflat -> BinOp of NAT means :Def1: :: NAT_LAT:def 1
for m, n being Nat holds it . (m,n) = m gcd n;
existence
ex b1 being BinOp of NAT st
for m, n being Nat holds b1 . (m,n) = m gcd n
proof
deffunc H1( Nat, Nat) -> Element of NAT = $1 gcd $2;
consider o being BinOp of NAT such that
A1: for a, b being Element of NAT holds o . (a,b) = H1(a,b) from BINOP_1:sch_4();
take o ; ::_thesis: for m, n being Nat holds o . (m,n) = m gcd n
let m, n be Nat; ::_thesis: o . (m,n) = m gcd n
( m in NAT & n in NAT ) by ORDINAL1:def_12;
hence o . (m,n) = m gcd n by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being BinOp of NAT st ( for m, n being Nat holds b1 . (m,n) = m gcd n ) & ( for m, n being Nat holds b2 . (m,n) = m gcd n ) holds
b1 = b2
proof
let f1, f2 be BinOp of NAT; ::_thesis: ( ( for m, n being Nat holds f1 . (m,n) = m gcd n ) & ( for m, n being Nat holds f2 . (m,n) = m gcd n ) implies f1 = f2 )
assume that
A2: for m, n being Nat holds f1 . (m,n) = m gcd n and
A3: for m, n being Nat holds f2 . (m,n) = m gcd n ; ::_thesis: f1 = f2
now__::_thesis:_for_m,_n_being_Element_of_NAT_holds_f1_._(m,n)_=_f2_._(m,n)
let m, n be Element of NAT ; ::_thesis: f1 . (m,n) = f2 . (m,n)
thus f1 . (m,n) = m gcd n by A2
.= f2 . (m,n) by A3 ; ::_thesis: verum
end;
hence f1 = f2 by BINOP_1:2; ::_thesis: verum
end;
func lcmlat -> BinOp of NAT means :Def2: :: NAT_LAT:def 2
for m, n being Nat holds it . (m,n) = m lcm n;
existence
ex b1 being BinOp of NAT st
for m, n being Nat holds b1 . (m,n) = m lcm n
proof
deffunc H1( Nat, Nat) -> Element of NAT = $1 lcm $2;
consider o being BinOp of NAT such that
A4: for a, b being Element of NAT holds o . (a,b) = H1(a,b) from BINOP_1:sch_4();
take o ; ::_thesis: for m, n being Nat holds o . (m,n) = m lcm n
let m, n be Nat; ::_thesis: o . (m,n) = m lcm n
( m in NAT & n in NAT ) by ORDINAL1:def_12;
hence o . (m,n) = m lcm n by A4; ::_thesis: verum
end;
uniqueness
for b1, b2 being BinOp of NAT st ( for m, n being Nat holds b1 . (m,n) = m lcm n ) & ( for m, n being Nat holds b2 . (m,n) = m lcm n ) holds
b1 = b2
proof
let f1, f2 be BinOp of NAT; ::_thesis: ( ( for m, n being Nat holds f1 . (m,n) = m lcm n ) & ( for m, n being Nat holds f2 . (m,n) = m lcm n ) implies f1 = f2 )
assume that
A5: for m, n being Nat holds f1 . (m,n) = m lcm n and
A6: for m, n being Nat holds f2 . (m,n) = m lcm n ; ::_thesis: f1 = f2
now__::_thesis:_for_m,_n_being_Element_of_NAT_holds_f1_._(m,n)_=_f2_._(m,n)
let m, n be Element of NAT ; ::_thesis: f1 . (m,n) = f2 . (m,n)
thus f1 . (m,n) = m lcm n by A5
.= f2 . (m,n) by A6 ; ::_thesis: verum
end;
hence f1 = f2 by BINOP_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines hcflat NAT_LAT:def_1_:_
for b1 being BinOp of NAT holds
( b1 = hcflat iff for m, n being Nat holds b1 . (m,n) = m gcd n );
:: deftheorem Def2 defines lcmlat NAT_LAT:def_2_:_
for b1 being BinOp of NAT holds
( b1 = lcmlat iff for m, n being Nat holds b1 . (m,n) = m lcm n );
definition
func Nat_Lattice -> non empty strict LattStr equals :: NAT_LAT:def 3
LattStr(# NAT,lcmlat,hcflat #);
coherence
LattStr(# NAT,lcmlat,hcflat #) is non empty strict LattStr ;
end;
:: deftheorem defines Nat_Lattice NAT_LAT:def_3_:_
Nat_Lattice = LattStr(# NAT,lcmlat,hcflat #);
registration
cluster the carrier of Nat_Lattice -> natural-membered ;
coherence
the carrier of Nat_Lattice is natural-membered ;
end;
registration
let p, q be Element of Nat_Lattice;
identifyp "\/" q with p lcm q;
compatibility
p "\/" q = p lcm q by Def2;
identifyp "/\" q with p gcd q;
compatibility
p "/\" q = p gcd q by Def1;
end;
theorem :: NAT_LAT:1
for p, q being Element of Nat_Lattice holds p "\/" q = p lcm q ;
theorem :: NAT_LAT:2
for p, q being Element of Nat_Lattice holds p "/\" q = p gcd q ;
theorem :: NAT_LAT:3
for a, b being Element of Nat_Lattice st a [= b holds
a divides b
proof
let a, b be Element of Nat_Lattice; ::_thesis: ( a [= b implies a divides b )
assume a [= b ; ::_thesis: a divides b
then a "\/" b = b by LATTICES:def_3;
hence a divides b by NEWTON:44; ::_thesis: verum
end;
definition
func 0_NN -> Element of Nat_Lattice equals :: NAT_LAT:def 4
1;
coherence
1 is Element of Nat_Lattice ;
func 1_NN -> Element of Nat_Lattice equals :: NAT_LAT:def 5
0 ;
coherence
0 is Element of Nat_Lattice ;
end;
:: deftheorem defines 0_NN NAT_LAT:def_4_:_
0_NN = 1;
:: deftheorem defines 1_NN NAT_LAT:def_5_:_
1_NN = 0 ;
theorem :: NAT_LAT:4
0_NN = 1 ;
Lm1: for a being Element of Nat_Lattice holds
( 0_NN "/\" a = 0_NN & a "/\" 0_NN = 0_NN )
by NEWTON:51;
registration
cluster Nat_Lattice -> non empty strict Lattice-like ;
coherence
Nat_Lattice is Lattice-like
proof
thus ( ( for p, q being Element of Nat_Lattice holds p "\/" q = q "\/" p ) & ( for p, q, r being Element of Nat_Lattice holds p "\/" (q "\/" r) = (p "\/" q) "\/" r ) & ( for p, q being Element of Nat_Lattice holds (p "/\" q) "\/" q = q ) & ( for p, q being Element of Nat_Lattice holds p "/\" q = q "/\" p ) & ( for p, q, r being Element of Nat_Lattice holds p "/\" (q "/\" r) = (p "/\" q) "/\" r ) & ( for p, q being Element of Nat_Lattice holds p "/\" (p "\/" q) = p ) ) by NEWTON:43, NEWTON:48, NEWTON:53, NEWTON:54; :: according to LATTICES:def_4,LATTICES:def_5,LATTICES:def_6,LATTICES:def_7,LATTICES:def_8,LATTICES:def_9,LATTICES:def_10 ::_thesis: verum
end;
end;
registration
cluster Nat_Lattice -> non empty strict ;
coherence
Nat_Lattice is strict ;
end;
registration
cluster Nat_Lattice -> non empty strict lower-bounded ;
coherence
Nat_Lattice is lower-bounded by Lm1, LATTICES:def_13;
end;
theorem Th5: :: NAT_LAT:5
for p, q being Element of Nat_Lattice holds lcmlat . (p,q) = lcmlat . (q,p)
proof
let p, q be Element of Nat_Lattice; ::_thesis: lcmlat . (p,q) = lcmlat . (q,p)
thus lcmlat . (p,q) = q "\/" p by LATTICES:def_1
.= lcmlat . (q,p) ; ::_thesis: verum
end;
theorem Th6: :: NAT_LAT:6
for q, p being Element of Nat_Lattice holds hcflat . (q,p) = hcflat . (p,q)
proof
let q, p be Element of Nat_Lattice; ::_thesis: hcflat . (q,p) = hcflat . (p,q)
thus hcflat . (q,p) = p "/\" q by LATTICES:def_2
.= hcflat . (p,q) ; ::_thesis: verum
end;
theorem Th7: :: NAT_LAT:7
for p, q, r being Element of Nat_Lattice holds lcmlat . (p,(lcmlat . (q,r))) = lcmlat . ((lcmlat . (p,q)),r)
proof
let p, q, r be Element of Nat_Lattice; ::_thesis: lcmlat . (p,(lcmlat . (q,r))) = lcmlat . ((lcmlat . (p,q)),r)
set s = q "\/" r;
thus lcmlat . (p,(lcmlat . (q,r))) = p "\/" (q "\/" r)
.= (p "\/" q) "\/" r by NEWTON:43
.= lcmlat . ((lcmlat . (p,q)),r) ; ::_thesis: verum
end;
theorem :: NAT_LAT:8
for p, q, r being Element of Nat_Lattice holds
( lcmlat . (p,(lcmlat . (q,r))) = lcmlat . ((lcmlat . (q,p)),r) & lcmlat . (p,(lcmlat . (q,r))) = lcmlat . ((lcmlat . (p,r)),q) & lcmlat . (p,(lcmlat . (q,r))) = lcmlat . ((lcmlat . (r,q)),p) & lcmlat . (p,(lcmlat . (q,r))) = lcmlat . ((lcmlat . (r,p)),q) )
proof
let p, q, r be Element of Nat_Lattice; ::_thesis: ( lcmlat . (p,(lcmlat . (q,r))) = lcmlat . ((lcmlat . (q,p)),r) & lcmlat . (p,(lcmlat . (q,r))) = lcmlat . ((lcmlat . (p,r)),q) & lcmlat . (p,(lcmlat . (q,r))) = lcmlat . ((lcmlat . (r,q)),p) & lcmlat . (p,(lcmlat . (q,r))) = lcmlat . ((lcmlat . (r,p)),q) )
set s = r "\/" q;
thus lcmlat . (p,(lcmlat . (q,r))) = lcmlat . ((lcmlat . (p,q)),r) by Th7
.= lcmlat . ((lcmlat . (q,p)),r) by Th5 ; ::_thesis: ( lcmlat . (p,(lcmlat . (q,r))) = lcmlat . ((lcmlat . (p,r)),q) & lcmlat . (p,(lcmlat . (q,r))) = lcmlat . ((lcmlat . (r,q)),p) & lcmlat . (p,(lcmlat . (q,r))) = lcmlat . ((lcmlat . (r,p)),q) )
thus A1: lcmlat . (p,(lcmlat . (q,r))) = lcmlat . (p,(lcmlat . (r,q))) by Th5
.= lcmlat . ((lcmlat . (p,r)),q) by Th7 ; ::_thesis: ( lcmlat . (p,(lcmlat . (q,r))) = lcmlat . ((lcmlat . (r,q)),p) & lcmlat . (p,(lcmlat . (q,r))) = lcmlat . ((lcmlat . (r,p)),q) )
thus lcmlat . (p,(lcmlat . (q,r))) = lcmlat . (p,(r "\/" q)) by LATTICES:def_1
.= lcmlat . ((lcmlat . (r,q)),p) by Th5 ; ::_thesis: lcmlat . (p,(lcmlat . (q,r))) = lcmlat . ((lcmlat . (r,p)),q)
thus lcmlat . (p,(lcmlat . (q,r))) = lcmlat . ((lcmlat . (r,p)),q) by A1, Th5; ::_thesis: verum
end;
theorem Th9: :: NAT_LAT:9
for p, q, r being Element of Nat_Lattice holds hcflat . (p,(hcflat . (q,r))) = hcflat . ((hcflat . (p,q)),r)
proof
let p, q, r be Element of Nat_Lattice; ::_thesis: hcflat . (p,(hcflat . (q,r))) = hcflat . ((hcflat . (p,q)),r)
set s = q "/\" r;
thus hcflat . (p,(hcflat . (q,r))) = p "/\" (q "/\" r)
.= (p "/\" q) "/\" r by NEWTON:48
.= hcflat . ((hcflat . (p,q)),r) ; ::_thesis: verum
end;
theorem :: NAT_LAT:10
for p, q, r being Element of Nat_Lattice holds
( hcflat . (p,(hcflat . (q,r))) = hcflat . ((hcflat . (q,p)),r) & hcflat . (p,(hcflat . (q,r))) = hcflat . ((hcflat . (p,r)),q) & hcflat . (p,(hcflat . (q,r))) = hcflat . ((hcflat . (r,q)),p) & hcflat . (p,(hcflat . (q,r))) = hcflat . ((hcflat . (r,p)),q) )
proof
let p, q, r be Element of Nat_Lattice; ::_thesis: ( hcflat . (p,(hcflat . (q,r))) = hcflat . ((hcflat . (q,p)),r) & hcflat . (p,(hcflat . (q,r))) = hcflat . ((hcflat . (p,r)),q) & hcflat . (p,(hcflat . (q,r))) = hcflat . ((hcflat . (r,q)),p) & hcflat . (p,(hcflat . (q,r))) = hcflat . ((hcflat . (r,p)),q) )
set s = r "/\" q;
thus hcflat . (p,(hcflat . (q,r))) = hcflat . ((hcflat . (p,q)),r) by Th9
.= hcflat . ((hcflat . (q,p)),r) by Th6 ; ::_thesis: ( hcflat . (p,(hcflat . (q,r))) = hcflat . ((hcflat . (p,r)),q) & hcflat . (p,(hcflat . (q,r))) = hcflat . ((hcflat . (r,q)),p) & hcflat . (p,(hcflat . (q,r))) = hcflat . ((hcflat . (r,p)),q) )
thus A1: hcflat . (p,(hcflat . (q,r))) = hcflat . (p,(hcflat . (r,q))) by Th6
.= hcflat . ((hcflat . (p,r)),q) by Th9 ; ::_thesis: ( hcflat . (p,(hcflat . (q,r))) = hcflat . ((hcflat . (r,q)),p) & hcflat . (p,(hcflat . (q,r))) = hcflat . ((hcflat . (r,p)),q) )
thus hcflat . (p,(hcflat . (q,r))) = hcflat . (p,(r "/\" q)) by LATTICES:def_2
.= hcflat . ((hcflat . (r,q)),p) by Th6 ; ::_thesis: hcflat . (p,(hcflat . (q,r))) = hcflat . ((hcflat . (r,p)),q)
thus hcflat . (p,(hcflat . (q,r))) = hcflat . ((hcflat . (r,p)),q) by A1, Th6; ::_thesis: verum
end;
theorem :: NAT_LAT:11
for q, p being Element of Nat_Lattice holds
( hcflat . (q,(lcmlat . (q,p))) = q & hcflat . ((lcmlat . (p,q)),q) = q & hcflat . (q,(lcmlat . (p,q))) = q & hcflat . ((lcmlat . (q,p)),q) = q )
proof
let q, p be Element of Nat_Lattice; ::_thesis: ( hcflat . (q,(lcmlat . (q,p))) = q & hcflat . ((lcmlat . (p,q)),q) = q & hcflat . (q,(lcmlat . (p,q))) = q & hcflat . ((lcmlat . (q,p)),q) = q )
set s = q "\/" p;
thus A1: hcflat . (q,(lcmlat . (q,p))) = q "/\" (q "\/" p)
.= q by NEWTON:54 ; ::_thesis: ( hcflat . ((lcmlat . (p,q)),q) = q & hcflat . (q,(lcmlat . (p,q))) = q & hcflat . ((lcmlat . (q,p)),q) = q )
thus A2: hcflat . ((lcmlat . (p,q)),q) = hcflat . ((p "\/" q),q)
.= q "/\" (q "\/" p) by LATTICES:def_2
.= q by NEWTON:54 ; ::_thesis: ( hcflat . (q,(lcmlat . (p,q))) = q & hcflat . ((lcmlat . (q,p)),q) = q )
thus hcflat . (q,(lcmlat . (p,q))) = q by A1, Th5; ::_thesis: hcflat . ((lcmlat . (q,p)),q) = q
thus hcflat . ((lcmlat . (q,p)),q) = q by A2, Th5; ::_thesis: verum
end;
theorem :: NAT_LAT:12
for q, p being Element of Nat_Lattice holds
( lcmlat . (q,(hcflat . (q,p))) = q & lcmlat . ((hcflat . (p,q)),q) = q & lcmlat . (q,(hcflat . (p,q))) = q & lcmlat . ((hcflat . (q,p)),q) = q )
proof
let q, p be Element of Nat_Lattice; ::_thesis: ( lcmlat . (q,(hcflat . (q,p))) = q & lcmlat . ((hcflat . (p,q)),q) = q & lcmlat . (q,(hcflat . (p,q))) = q & lcmlat . ((hcflat . (q,p)),q) = q )
set r = p "/\" q;
thus A1: lcmlat . (q,(hcflat . (q,p))) = lcmlat . (q,(q "/\" p))
.= (p "/\" q) "\/" q by LATTICES:def_1
.= q by NEWTON:53 ; ::_thesis: ( lcmlat . ((hcflat . (p,q)),q) = q & lcmlat . (q,(hcflat . (p,q))) = q & lcmlat . ((hcflat . (q,p)),q) = q )
thus A2: lcmlat . ((hcflat . (p,q)),q) = (p "/\" q) "\/" q
.= q by NEWTON:53 ; ::_thesis: ( lcmlat . (q,(hcflat . (p,q))) = q & lcmlat . ((hcflat . (q,p)),q) = q )
thus lcmlat . (q,(hcflat . (p,q))) = q by A1, Th6; ::_thesis: lcmlat . ((hcflat . (q,p)),q) = q
thus lcmlat . ((hcflat . (q,p)),q) = q by A2, Th6; ::_thesis: verum
end;
definition
func NATPLUS -> Subset of NAT means :Def6: :: NAT_LAT:def 6
for n being Nat holds
( n in it iff 0 < n );
existence
ex b1 being Subset of NAT st
for n being Nat holds
( n in b1 iff 0 < n )
proof
defpred S1[ Nat] means 0 < $1;
consider X being Subset of NAT such that
A1: for n being Element of NAT holds
( n in X iff S1[n] ) from SUBSET_1:sch_3();
take X ; ::_thesis: for n being Nat holds
( n in X iff 0 < n )
let n be Nat; ::_thesis: ( n in X iff 0 < n )
thus ( n in X implies 0 < n ) by A1; ::_thesis: ( 0 < n implies n in X )
n in NAT by ORDINAL1:def_12;
hence ( 0 < n implies n in X ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset of NAT st ( for n being Nat holds
( n in b1 iff 0 < n ) ) & ( for n being Nat holds
( n in b2 iff 0 < n ) ) holds
b1 = b2
proof
let X, Y be Subset of NAT; ::_thesis: ( ( for n being Nat holds
( n in X iff 0 < n ) ) & ( for n being Nat holds
( n in Y iff 0 < n ) ) implies X = Y )
assume that
A2: for n being Nat holds
( n in X iff 0 < n ) and
A3: for n being Nat holds
( n in Y iff 0 < n ) ; ::_thesis: X = Y
thus X c= Y :: according to XBOOLE_0:def_10 ::_thesis: Y c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in Y )
assume A4: x in X ; ::_thesis: x in Y
then reconsider x = x as Nat ;
0 < x by A2, A4;
hence x in Y by A3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Y or x in X )
assume A5: x in Y ; ::_thesis: x in X
then reconsider x = x as Nat ;
0 < x by A3, A5;
hence x in X by A2; ::_thesis: verum
end;
end;
:: deftheorem Def6 defines NATPLUS NAT_LAT:def_6_:_
for b1 being Subset of NAT holds
( b1 = NATPLUS iff for n being Nat holds
( n in b1 iff 0 < n ) );
registration
cluster NATPLUS -> non empty ;
coherence
not NATPLUS is empty
proof
0 < 1 ;
hence not NATPLUS is empty by Def6; ::_thesis: verum
end;
end;
definition
let D be non empty set ;
let S be non empty Subset of D;
let N be non empty Subset of S;
:: original: Element
redefine mode Element of N -> Element of S;
coherence
for b1 being Element of N holds b1 is Element of S
proof
let x be Element of N; ::_thesis: x is Element of S
thus x is Element of S ; ::_thesis: verum
end;
end;
registration
let D be Subset of REAL;
cluster -> real for Element of D;
coherence
for b1 being Element of D holds b1 is real ;
end;
registration
let D be Subset of NAT;
cluster -> real for Element of D;
coherence
for b1 being Element of D holds b1 is real ;
end;
definition
mode NatPlus is Element of NATPLUS ;
end;
definition
let k be Nat;
assume A1: k > 0 ;
func @ k -> NatPlus equals :Def7: :: NAT_LAT:def 7
k;
coherence
k is NatPlus by A1, Def6;
end;
:: deftheorem Def7 defines @ NAT_LAT:def_7_:_
for k being Nat st k > 0 holds
@ k = k;
registration
cluster -> non zero natural for Element of NATPLUS ;
coherence
for b1 being NatPlus holds
( b1 is natural & not b1 is zero ) by Def6;
end;
definition
func hcflatplus -> BinOp of NATPLUS means :Def8: :: NAT_LAT:def 8
for m, n being NatPlus holds it . (m,n) = m gcd n;
existence
ex b1 being BinOp of NATPLUS st
for m, n being NatPlus holds b1 . (m,n) = m gcd n
proof
deffunc H1( NatPlus, NatPlus) -> NatPlus = @ ($1 gcd $2);
consider f being BinOp of NATPLUS such that
A1: for m, n being NatPlus holds f . (m,n) = H1(m,n) from BINOP_1:sch_4();
take f ; ::_thesis: for m, n being NatPlus holds f . (m,n) = m gcd n
let m, n be NatPlus; ::_thesis: f . (m,n) = m gcd n
A2: f . (m,n) = @ (m gcd n) by A1;
n > 0 by Def6;
hence f . (m,n) = m gcd n by A2, Def7, NEWTON:58; ::_thesis: verum
end;
uniqueness
for b1, b2 being BinOp of NATPLUS st ( for m, n being NatPlus holds b1 . (m,n) = m gcd n ) & ( for m, n being NatPlus holds b2 . (m,n) = m gcd n ) holds
b1 = b2
proof
deffunc H1( NatPlus, NatPlus) -> Element of NAT = $1 gcd $2;
thus for o1, o2 being BinOp of NATPLUS st ( for a, b being NatPlus holds o1 . (a,b) = H1(a,b) ) & ( for a, b being NatPlus holds o2 . (a,b) = H1(a,b) ) holds
o1 = o2 from BINOP_2:sch_2(); ::_thesis: verum
end;
func lcmlatplus -> BinOp of NATPLUS means :Def9: :: NAT_LAT:def 9
for m, n being NatPlus holds it . (m,n) = m lcm n;
existence
ex b1 being BinOp of NATPLUS st
for m, n being NatPlus holds b1 . (m,n) = m lcm n
proof
deffunc H1( NatPlus, NatPlus) -> NatPlus = @ ($1 lcm $2);
consider f being BinOp of NATPLUS such that
A3: for m, n being NatPlus holds f . (m,n) = H1(m,n) from BINOP_1:sch_4();
take f ; ::_thesis: for m, n being NatPlus holds f . (m,n) = m lcm n
let m, n be NatPlus; ::_thesis: f . (m,n) = m lcm n
A4: ( m > 0 & n > 0 ) by Def6;
thus f . (m,n) = H1(m,n) by A3
.= m lcm n by A4, Def7, NEWTON:59 ; ::_thesis: verum
end;
uniqueness
for b1, b2 being BinOp of NATPLUS st ( for m, n being NatPlus holds b1 . (m,n) = m lcm n ) & ( for m, n being NatPlus holds b2 . (m,n) = m lcm n ) holds
b1 = b2
proof
deffunc H1( NatPlus, NatPlus) -> Element of NAT = $1 lcm $2;
thus for o1, o2 being BinOp of NATPLUS st ( for a, b being NatPlus holds o1 . (a,b) = H1(a,b) ) & ( for a, b being NatPlus holds o2 . (a,b) = H1(a,b) ) holds
o1 = o2 from BINOP_2:sch_2(); ::_thesis: verum
end;
end;
:: deftheorem Def8 defines hcflatplus NAT_LAT:def_8_:_
for b1 being BinOp of NATPLUS holds
( b1 = hcflatplus iff for m, n being NatPlus holds b1 . (m,n) = m gcd n );
:: deftheorem Def9 defines lcmlatplus NAT_LAT:def_9_:_
for b1 being BinOp of NATPLUS holds
( b1 = lcmlatplus iff for m, n being NatPlus holds b1 . (m,n) = m lcm n );
definition
func NatPlus_Lattice -> strict LattStr equals :: NAT_LAT:def 10
LattStr(# NATPLUS,lcmlatplus,hcflatplus #);
coherence
LattStr(# NATPLUS,lcmlatplus,hcflatplus #) is strict LattStr ;
end;
:: deftheorem defines NatPlus_Lattice NAT_LAT:def_10_:_
NatPlus_Lattice = LattStr(# NATPLUS,lcmlatplus,hcflatplus #);
registration
cluster NatPlus_Lattice -> non empty strict ;
coherence
not NatPlus_Lattice is empty ;
end;
definition
let m be Element of NatPlus_Lattice;
func @ m -> NatPlus equals :: NAT_LAT:def 11
m;
coherence
m is NatPlus ;
end;
:: deftheorem defines @ NAT_LAT:def_11_:_
for m being Element of NatPlus_Lattice holds @ m = m;
registration
cluster -> non zero natural for Element of the carrier of NatPlus_Lattice;
coherence
for b1 being Element of NatPlus_Lattice holds
( b1 is natural & not b1 is zero ) ;
end;
registration
let p, q be Element of NatPlus_Lattice;
identifyp "\/" q with p lcm q;
compatibility
p "\/" q = p lcm q by Def9;
identifyp "/\" q with p gcd q;
compatibility
p "/\" q = p gcd q by Def8;
end;
theorem :: NAT_LAT:13
for p, q being Element of NatPlus_Lattice holds p "\/" q = (@ p) lcm (@ q) ;
theorem :: NAT_LAT:14
for p, q being Element of NatPlus_Lattice holds p "/\" q = (@ p) gcd (@ q) ;
Lm2: ( ( for a, b being Element of NatPlus_Lattice holds a "\/" b = b "\/" a ) & ( for a, b, c being Element of NatPlus_Lattice holds a "\/" (b "\/" c) = (a "\/" b) "\/" c ) )
by NEWTON:43;
Lm3: ( ( for a, b being Element of NatPlus_Lattice holds (a "/\" b) "\/" b = b ) & ( for a, b being Element of NatPlus_Lattice holds a "/\" b = b "/\" a ) )
by NEWTON:53;
Lm4: ( ( for a, b, c being Element of NatPlus_Lattice holds a "/\" (b "/\" c) = (a "/\" b) "/\" c ) & ( for a, b being Element of NatPlus_Lattice holds a "/\" (a "\/" b) = a ) )
by NEWTON:48, NEWTON:54;
registration
cluster NatPlus_Lattice -> strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing ;
coherence
( NatPlus_Lattice is join-commutative & NatPlus_Lattice is join-associative & NatPlus_Lattice is meet-commutative & NatPlus_Lattice is meet-associative & NatPlus_Lattice is join-absorbing & NatPlus_Lattice is meet-absorbing ) by Lm2, Lm3, Lm4, LATTICES:def_4, LATTICES:def_5, LATTICES:def_6, LATTICES:def_7, LATTICES:def_8, LATTICES:def_9;
end;
Lm5: now__::_thesis:_for_L_being_Lattice_holds_
(_the_L_join_of_L_=_the_L_join_of_L_||_the_carrier_of_L_&_the_L_meet_of_L_=_the_L_meet_of_L_||_the_carrier_of_L_)
let L be Lattice; ::_thesis: ( the L_join of L = the L_join of L || the carrier of L & the L_meet of L = the L_meet of L || the carrier of L )
[: the carrier of L, the carrier of L:] = dom the L_join of L by FUNCT_2:def_1;
hence the L_join of L = the L_join of L || the carrier of L by RELAT_1:68; ::_thesis: the L_meet of L = the L_meet of L || the carrier of L
[: the carrier of L, the carrier of L:] = dom the L_meet of L by FUNCT_2:def_1;
hence the L_meet of L = the L_meet of L || the carrier of L by RELAT_1:68; ::_thesis: verum
end;
definition
let L be Lattice;
mode SubLattice of L -> Lattice means :Def12: :: NAT_LAT:def 12
( 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 Lattice 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
take L ; ::_thesis: ( the carrier of L c= the carrier of L & the L_join of L = the L_join of L || the carrier of L & the L_meet of L = the L_meet of L || the carrier of L )
thus ( the carrier of L c= the carrier of L & the L_join of L = the L_join of L || the carrier of L & the L_meet of L = the L_meet of L || the carrier of L ) by Lm5; ::_thesis: verum
end;
end;
:: deftheorem Def12 defines SubLattice NAT_LAT:def_12_:_
for L, b2 being Lattice holds
( b2 is SubLattice 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 Lattice;
cluster non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like for SubLattice of L;
existence
ex b1 being SubLattice of L st b1 is strict
proof
set S = LattStr(# the carrier of L, the L_join of L, the L_meet of L #);
A1: now__::_thesis:_for_a,_b,_c_being_Element_of_LattStr(#_the_carrier_of_L,_the_L_join_of_L,_the_L_meet_of_L_#)_holds_a_"\/"_(b_"\/"_c)_=_(a_"\/"_b)_"\/"_c
let a, b, c be Element of LattStr(# the carrier of L, the L_join of L, the L_meet of L #); ::_thesis: a "\/" (b "\/" c) = (a "\/" b) "\/" c
reconsider a9 = a, b9 = b, c9 = c as Element of L ;
thus a "\/" (b "\/" c) = a9 "\/" (b9 "\/" c9)
.= (a9 "\/" b9) "\/" c9 by LATTICES:def_5
.= (a "\/" b) "\/" c ; ::_thesis: verum
end;
A2: now__::_thesis:_for_a,_b_being_Element_of_LattStr(#_the_carrier_of_L,_the_L_join_of_L,_the_L_meet_of_L_#)_holds_(a_"/\"_b)_"\/"_b_=_b
let a, b be Element of LattStr(# the carrier of L, the L_join of L, the L_meet of L #); ::_thesis: (a "/\" b) "\/" b = b
reconsider a9 = a, b9 = b as Element of L ;
thus (a "/\" b) "\/" b = (a9 "/\" b9) "\/" b9
.= b by LATTICES:def_8 ; ::_thesis: verum
end;
A3: now__::_thesis:_for_a,_b_being_Element_of_LattStr(#_the_carrier_of_L,_the_L_join_of_L,_the_L_meet_of_L_#)_holds_a_"/\"_(a_"\/"_b)_=_a
let a, b be Element of LattStr(# the carrier of L, the L_join of L, the L_meet of L #); ::_thesis: a "/\" (a "\/" b) = a
reconsider a9 = a, b9 = b as Element of L ;
thus a "/\" (a "\/" b) = a9 "/\" (a9 "\/" b9)
.= a by LATTICES:def_9 ; ::_thesis: verum
end;
A4: now__::_thesis:_for_a,_b,_c_being_Element_of_LattStr(#_the_carrier_of_L,_the_L_join_of_L,_the_L_meet_of_L_#)_holds_a_"/\"_(b_"/\"_c)_=_(a_"/\"_b)_"/\"_c
let a, b, c be Element of LattStr(# the carrier of L, the L_join of L, the L_meet of L #); ::_thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c
reconsider a9 = a, b9 = b, c9 = c as Element of L ;
thus a "/\" (b "/\" c) = a9 "/\" (b9 "/\" c9)
.= (a9 "/\" b9) "/\" c9 by LATTICES:def_7
.= (a "/\" b) "/\" c ; ::_thesis: verum
end;
A5: for a, b being Element of LattStr(# the carrier of L, the L_join of L, the L_meet of L #)
for a9, b9 being Element of L st a = a9 & b = b9 holds
( a "\/" b = a9 "\/" b9 & a "/\" b = a9 "/\" b9 ) ;
A6: now__::_thesis:_for_a,_b_being_Element_of_LattStr(#_the_carrier_of_L,_the_L_join_of_L,_the_L_meet_of_L_#)_holds_a_"/\"_b_=_b_"/\"_a
let a, b be Element of LattStr(# the carrier of L, the L_join of L, the L_meet of L #); ::_thesis: a "/\" b = b "/\" a
reconsider a9 = a, b9 = b as Element of L ;
thus a "/\" b = b9 "/\" a9 by A5
.= b "/\" a ; ::_thesis: verum
end;
now__::_thesis:_for_a,_b_being_Element_of_LattStr(#_the_carrier_of_L,_the_L_join_of_L,_the_L_meet_of_L_#)_holds_a_"\/"_b_=_b_"\/"_a
let a, b be Element of LattStr(# the carrier of L, the L_join of L, the L_meet of L #); ::_thesis: a "\/" b = b "\/" a
reconsider a9 = a, b9 = b as Element of L ;
thus a "\/" b = b9 "\/" a9 by A5
.= b "\/" a ; ::_thesis: verum
end;
then ( LattStr(# the carrier of L, the L_join of L, the L_meet of L #) is join-commutative & LattStr(# the carrier of L, the L_join of L, the L_meet of L #) is join-associative & LattStr(# the carrier of L, the L_join of L, the L_meet of L #) is meet-absorbing & LattStr(# the carrier of L, the L_join of L, the L_meet of L #) is meet-commutative & LattStr(# the carrier of L, the L_join of L, the L_meet of L #) is meet-associative & LattStr(# the carrier of L, the L_join of L, the L_meet of L #) is join-absorbing ) by A1, A2, A6, A4, A3, LATTICES:def_4, LATTICES:def_5, LATTICES:def_6, LATTICES:def_7, LATTICES:def_8, LATTICES:def_9;
then reconsider S = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) as Lattice ;
( the L_join of S = the L_join of L || the carrier of S & the L_meet of S = the L_meet of L || the carrier of S ) by RELSET_1:19;
then S is SubLattice of L by Def12;
hence ex b1 being SubLattice of L st b1 is strict ; ::_thesis: verum
end;
end;
theorem :: NAT_LAT:15
for L being Lattice holds L is SubLattice of L
proof
let L be Lattice; ::_thesis: L is SubLattice of L
thus the carrier of L c= the carrier of L ; :: according to NAT_LAT:def_12 ::_thesis: ( the L_join of L = the L_join of L || the carrier of L & the L_meet of L = the L_meet of L || the carrier of L )
thus ( the L_join of L = the L_join of L || the carrier of L & the L_meet of L = the L_meet of L || the carrier of L ) by Lm5; ::_thesis: verum
end;
theorem :: NAT_LAT:16
NatPlus_Lattice is SubLattice of Nat_Lattice
proof
A1: for x being set st x in dom hcflatplus holds
hcflatplus . x = hcflat . x
proof
let x be set ; ::_thesis: ( x in dom hcflatplus implies hcflatplus . x = hcflat . x )
assume A2: x in dom hcflatplus ; ::_thesis: hcflatplus . x = hcflat . x
then A3: x in [:NATPLUS,NATPLUS:] by FUNCT_2:def_1;
consider y1, y2 being set such that
A4: [y1,y2] = x by A2, RELAT_1:def_1;
( y1 in NATPLUS & y2 in NATPLUS ) by A3, A4, ZFMISC_1:87;
then reconsider n = y1, k = y2 as Nat ;
A5: hcflat . (n,k) = n gcd k by Def1;
reconsider n = y1, k = y2 as NatPlus by A3, A4, ZFMISC_1:87;
hcflatplus . (n,k) = hcflat . (n,k) by A5, Def8;
hence hcflatplus . x = hcflat . x by A4; ::_thesis: verum
end;
( dom hcflatplus = [:NATPLUS,NATPLUS:] & dom hcflat = [:NAT,NAT:] ) by FUNCT_2:def_1;
then dom hcflatplus = (dom hcflat) /\ [:NATPLUS,NATPLUS:] by XBOOLE_1:28, ZFMISC_1:96;
then A6: hcflatplus = hcflat || NATPLUS by A1, FUNCT_1:46;
A7: for x being set st x in dom lcmlatplus holds
lcmlatplus . x = lcmlat . x
proof
let x be set ; ::_thesis: ( x in dom lcmlatplus implies lcmlatplus . x = lcmlat . x )
assume A8: x in dom lcmlatplus ; ::_thesis: lcmlatplus . x = lcmlat . x
then A9: x in [:NATPLUS,NATPLUS:] by FUNCT_2:def_1;
consider y1, y2 being set such that
A10: [y1,y2] = x by A8, RELAT_1:def_1;
( y1 in NATPLUS & y2 in NATPLUS ) by A9, A10, ZFMISC_1:87;
then reconsider n = y1, k = y2 as Nat ;
A11: lcmlat . (n,k) = n lcm k by Def2;
reconsider n = y1, k = y2 as NatPlus by A9, A10, ZFMISC_1:87;
lcmlatplus . (n,k) = lcmlat . (n,k) by A11, Def9;
hence lcmlatplus . x = lcmlat . x by A10; ::_thesis: verum
end;
( dom lcmlatplus = [:NATPLUS,NATPLUS:] & dom lcmlat = [:NAT,NAT:] ) by FUNCT_2:def_1;
then dom lcmlatplus = (dom lcmlat) /\ [:NATPLUS,NATPLUS:] by XBOOLE_1:28, ZFMISC_1:96;
then lcmlatplus = lcmlat || NATPLUS by A7, FUNCT_1:46;
hence NatPlus_Lattice is SubLattice of Nat_Lattice by A6, Def12; ::_thesis: verum
end;