Step
*
of Lemma
divisibility-lattice_wf
divisibility-lattice() ∈ Lattice
BY
{ ((RepUR ``divisibility-lattice`` 0 THEN MemCD) THEN RepUR ``so_apply`` 0 THEN Auto) }
1
.....wf..... 
1. ∀[a,b:ℕ].  (gcd(a;b) = gcd(b;a) ∈ ℕ)
2. ∀[a,b:ℕ].  (lcm(a;b) = lcm(b;a) ∈ ℕ)
3. a : ℕ
4. b : ℕ
5. c : ℕ
⊢ gcd(a;gcd(b;c)) ∈ ℕ
Latex:
Latex:
divisibility-lattice()  \mmember{}  Lattice
By
Latex:
((RepUR  ``divisibility-lattice``  0  THEN  MemCD)  THEN  RepUR  ``so\_apply``  0  THEN  Auto)
Home
Index