Step * of Lemma divisibility-lattice_wf

divisibility-lattice() ∈ Lattice
BY
((RepUR ``divisibility-lattice`` THEN MemCD) THEN RepUR ``so_apply`` THEN Auto) }

1
.....wf..... 
1. ∀[a,b:ℕ].  (gcd(a;b) gcd(b;a) ∈ ℕ)
2. ∀[a,b:ℕ].  (lcm(a;b) lcm(b;a) ∈ ℕ)
3. : ℕ
4. : ℕ
5. : ℕ
⊢ 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