---

Step * of Lemma qadd_grp_wf

No Annotations
<ℚ+> ∈ AbGrp
BY
{ TACTIC:(Unfold `qadd_grp` 0 THEN (MemTypeCD THENA Auto)) }

1
<ℚ, λx,y. qeq(x;y), λx,y. q_le(x;y), λx,y. (x + y), 0, λx.-(x)> ∈ Group{i}

2
.....set predicate..... 
Comm(|<ℚ, λx,y. qeq(x;y), λx,y. q_le(x;y), λx,y. (x + y), 0, λx.-(x)>|;*)

---

Latex:

---

Latex:
No  Annotations
<\mBbbQ{}+>  \mmember{}  AbGrp


By

---

Latex:
TACTIC:(Unfold  `qadd\_grp`  0  THEN  (MemTypeCD  THENA  Auto))

---

Home Index