---

Step * of Lemma divisibility-lattice_wf

No Annotations
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:
No  Annotations
divisibility-lattice()  \mmember{}  Lattice


By

---

Latex:
((RepUR  ``divisibility-lattice``  0  THEN  MemCD)  THEN  RepUR  ``so\_apply``  0  THEN  Auto)

---

Home Index