:: NAT_LAT semantic presentation

definition

canceled;
canceled;
func hcflat -> BinOp of NAT means :Def3: :: NAT_LAT:def 3
for m, n being Nat holds it . m,n = m hcf n;
existence

proof end;

uniqueness

proof end;

func lcmlat -> BinOp of NAT means :Def4: :: NAT_LAT:def 4
for m, n being Nat holds it . m,n = m lcm n;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem NAT_LAT:def 1 :

:: deftheorem NAT_LAT:def 2 :

:: deftheorem Def3 defines hcflat NAT_LAT:def 3 :

:: deftheorem Def4 defines lcmlat NAT_LAT:def 4 :

definition

let m be Element of LattStr(# NAT ,lcmlat ,hcflat #);
func @ m -> Nat equals :: NAT_LAT:def 5
m;
coherence ;

end;

:: deftheorem defines @ NAT_LAT:def 5 :

theorem :: NAT_LAT:1

canceled;

theorem :: NAT_LAT:2

canceled;

theorem :: NAT_LAT:3

canceled;

theorem :: NAT_LAT:4

canceled;

theorem :: NAT_LAT:5

canceled;

theorem :: NAT_LAT:6

canceled;

theorem :: NAT_LAT:7

canceled;

theorem :: NAT_LAT:8

canceled;

theorem :: NAT_LAT:9

canceled;

theorem :: NAT_LAT:10

canceled;

theorem :: NAT_LAT:11

canceled;

theorem :: NAT_LAT:12

canceled;

theorem :: NAT_LAT:13

canceled;

theorem :: NAT_LAT:14

canceled;

theorem :: NAT_LAT:15

canceled;

theorem :: NAT_LAT:16

canceled;

theorem :: NAT_LAT:17

canceled;

theorem :: NAT_LAT:18

canceled;

theorem :: NAT_LAT:19

canceled;

theorem :: NAT_LAT:20

canceled;

theorem :: NAT_LAT:21

canceled;

theorem :: NAT_LAT:22

canceled;

theorem :: NAT_LAT:23

canceled;

theorem :: NAT_LAT:24

canceled;

theorem :: NAT_LAT:25

canceled;

theorem :: NAT_LAT:26

canceled;

theorem :: NAT_LAT:27

canceled;

theorem :: NAT_LAT:28

canceled;

theorem :: NAT_LAT:29

canceled;

theorem :: NAT_LAT:30

canceled;

theorem :: NAT_LAT:31

canceled;

theorem :: NAT_LAT:32

canceled;

theorem :: NAT_LAT:33

canceled;

theorem :: NAT_LAT:34

canceled;

theorem :: NAT_LAT:35

canceled;

theorem :: NAT_LAT:36

canceled;

theorem :: NAT_LAT:37

canceled;

theorem :: NAT_LAT:38

canceled;

theorem :: NAT_LAT:39

canceled;

theorem :: NAT_LAT:40

canceled;

theorem :: NAT_LAT:41

canceled;

theorem :: NAT_LAT:42

canceled;

theorem :: NAT_LAT:43

canceled;

theorem :: NAT_LAT:44

canceled;

theorem :: NAT_LAT:45

canceled;

theorem :: NAT_LAT:46

canceled;

theorem :: NAT_LAT:47

canceled;

theorem Th48: :: NAT_LAT:48

for p, q being Element of LattStr(# NAT ,lcmlat ,hcflat #) holds p "\/" q = (@ p) lcm (@ q) by Def4;

theorem Th49: :: NAT_LAT:49

for p, q being Element of LattStr(# NAT ,lcmlat ,hcflat #) holds p "/\" q = (@ p) hcf (@ q) by Def3;

Lm1: for a, b being Element of LattStr(# NAT ,lcmlat ,hcflat #) holds a "\/" b = b "\/" a

proof end;

Lm2: for a, b being Element of LattStr(# NAT ,lcmlat ,hcflat #) holds a "/\" b = b "/\" a

proof end;

Lm3: for a, b, c being Element of LattStr(# NAT ,lcmlat ,hcflat #) holds a "/\" (b "/\" c) = (a "/\" b) "/\" c

proof end;

Lm4: for a, b, c being Element of LattStr(# NAT ,lcmlat ,hcflat #) holds a "\/" (b "\/" c) = (a "\/" b) "\/" c

proof end;

Lm5: for a, b being Element of LattStr(# NAT ,lcmlat ,hcflat #) holds (a "/\" b) "\/" b = b

proof end;

Lm6: for a, b being Element of LattStr(# NAT ,lcmlat ,hcflat #) holds a "/\" (a "\/" b) = a

proof end;

theorem :: NAT_LAT:50

canceled;

theorem :: NAT_LAT:51

canceled;

theorem :: NAT_LAT:52

for a, b being Element of LattStr(# NAT ,lcmlat ,hcflat #) st a [= b holds
@ a divides @ b

proof end;

definition

func 0_NN -> Element of LattStr(# NAT ,lcmlat ,hcflat #) equals :: NAT_LAT:def 6
1;
coherence ;
func 1_NN -> Element of LattStr(# NAT ,lcmlat ,hcflat #) equals :: NAT_LAT:def 7
0;
coherence ;

end;

:: deftheorem defines 0_NN NAT_LAT:def 6 :

:: deftheorem defines 1_NN NAT_LAT:def 7 :

theorem :: NAT_LAT:53

canceled;

theorem :: NAT_LAT:54

canceled;

theorem Th55: :: NAT_LAT:55

@ 0_NN = 1 ;

theorem Th56: :: NAT_LAT:56

for a being Element of LattStr(# NAT ,lcmlat ,hcflat #) holds
( 0_NN "/\" a = 0_NN & a "/\" 0_NN = 0_NN )

proof end;

definition

func Nat_Lattice -> Lattice equals :: NAT_LAT:def 8
LattStr(# NAT ,lcmlat ,hcflat #);
coherence

proof end;

end;

:: deftheorem defines Nat_Lattice NAT_LAT:def 8 :

registration

cluster Nat_Lattice -> strict ;
coherence ;

end;

theorem :: NAT_LAT:57

canceled;

theorem :: NAT_LAT:58

canceled;

theorem :: NAT_LAT:59

canceled;

theorem :: NAT_LAT:60

Nat_Lattice is 0_Lattice by Th56, LATTICES:def 13;

theorem Th61: :: NAT_LAT:61

for p, q being Element of Nat_Lattice holds lcmlat . p,q = lcmlat . q,p

proof end;

theorem Th62: :: NAT_LAT:62

for q, p being Element of Nat_Lattice holds hcflat . q,p = hcflat . p,q

proof end;

theorem Th63: :: NAT_LAT:63

for p, q, r being Element of Nat_Lattice holds lcmlat . p,(lcmlat . q,r) = lcmlat . (lcmlat . p,q),r

proof end;

theorem :: NAT_LAT:64

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

theorem Th65: :: NAT_LAT:65

for p, q, r being Element of Nat_Lattice holds hcflat . p,(hcflat . q,r) = hcflat . (hcflat . p,q),r

proof end;

theorem :: NAT_LAT:66

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

theorem :: NAT_LAT:67

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

theorem :: NAT_LAT:68

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

definition

func NATPLUS -> Subset of NAT means :Def9: :: NAT_LAT:def 9
for n being Nat holds
( n in it iff 0 < n );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines NATPLUS NAT_LAT:def 9 :

registration

cluster NATPLUS -> non empty ;
coherence

proof 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

proof end;

end;

registration

let D be Subset of REAL ;
cluster -> real Element of D;
coherence ;

end;

registration

let D be Subset of NAT ;
cluster -> real Element of D;
coherence ;

end;

definition

mode NatPlus is Element of NATPLUS ;

end;

definition

let k be Nat;
assume A1: k > 0 ;
func @ k -> Element of NATPLUS equals :Def10: :: NAT_LAT:def 10
k;
coherence by A1, Def9;

end;

:: deftheorem Def10 defines @ NAT_LAT:def 10 :

definition

let k be Element of NATPLUS ;
func @ k -> NatPlus equals :: NAT_LAT:def 11
k;
coherence ;

end;

:: deftheorem defines @ NAT_LAT:def 11 :

definition

func hcflatplus -> BinOp of NATPLUS means :Def12: :: NAT_LAT:def 12
for m, n being NatPlus holds it . m,n = m hcf n;
existence

proof end;

uniqueness

proof end;

func lcmlatplus -> BinOp of NATPLUS means :Def13: :: NAT_LAT:def 13
for m, n being NatPlus holds it . m,n = m lcm n;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines hcflatplus NAT_LAT:def 12 :

:: deftheorem Def13 defines lcmlatplus NAT_LAT:def 13 :

definition

let m be Element of LattStr(# NATPLUS ,lcmlatplus ,hcflatplus #);
func @ m -> NatPlus equals :: NAT_LAT:def 14
m;
coherence ;

end;

:: deftheorem defines @ NAT_LAT:def 14 :

theorem Th69: :: NAT_LAT:69

for p, q being Element of LattStr(# NATPLUS ,lcmlatplus ,hcflatplus #) holds p "\/" q = (@ p) lcm (@ q) by Def13;

theorem Th70: :: NAT_LAT:70

for p, q being Element of LattStr(# NATPLUS ,lcmlatplus ,hcflatplus #) holds p "/\" q = (@ p) hcf (@ q) by Def12;

Lm7: for a, b being Element of LattStr(# NATPLUS ,lcmlatplus ,hcflatplus #) holds a "\/" b = b "\/" a

proof end;

Lm8: for a, b, c being Element of LattStr(# NATPLUS ,lcmlatplus ,hcflatplus #) holds a "\/" (b "\/" c) = (a "\/" b) "\/" c

proof end;

Lm9: for a, b being Element of LattStr(# NATPLUS ,lcmlatplus ,hcflatplus #) holds (a "/\" b) "\/" b = b

proof end;

Lm10: for a, b being Element of LattStr(# NATPLUS ,lcmlatplus ,hcflatplus #) holds a "/\" b = b "/\" a

proof end;

Lm11: for a, b, c being Element of LattStr(# NATPLUS ,lcmlatplus ,hcflatplus #) holds a "/\" (b "/\" c) = (a "/\" b) "/\" c

proof end;

Lm12: for a, b being Element of LattStr(# NATPLUS ,lcmlatplus ,hcflatplus #) holds a "/\" (a "\/" b) = a

proof end;

definition

func NatPlus_Lattice -> Lattice equals :: NAT_LAT:def 15
LattStr(# NATPLUS ,lcmlatplus ,hcflatplus #);
coherence

proof end;

end;

:: deftheorem defines NatPlus_Lattice NAT_LAT:def 15 :

registration

cluster NatPlus_Lattice -> strict ;
coherence ;

end;

Lm13: now

let L be Lattice; :: thesis:
thus the L_join of L = the L_join of L || the carrier of L :: thesis:

proof

[: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:97; :: thesis:

end;

thus the L_meet of L = the L_meet of L || the carrier of L :: thesis:

proof

[: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:97; :: thesis:

end;

definition