---

Step * 1 of Lemma qadd_grp_wf2


<ℚ+> ∈ OCMon
BY
{ TACTIC:(MemTypeCD THENW Auto) }

1
<ℚ+> ∈ AbMon

2
.....set predicate..... 
(UniformLinorder(|<ℚ+>|;x,y.↑(x ≤b y)) ∧ (=b = (λx,y. ((x ≤b y) ∧b (y ≤b x))) ∈ (|<ℚ+>| ⟶ |<ℚ+>| ⟶ 𝔹)))
∧ Cancel(|<ℚ+>|;|<ℚ+>|;*)
∧ (∀[z:|<ℚ+>|]. monot(|<ℚ+>|;x,y.↑(x ≤b y);λw.(z * w)))

---

Latex:

---

Latex:

<\mBbbQ{}+>  \mmember{}  OCMon


By

---

Latex:
TACTIC:(MemTypeCD  THENW  Auto)

---

Home Index