---

Step * of Lemma mk_abmonoid

∀[T:Type]. ∀[eq,le:T ⟶ T ⟶ 𝔹]. ∀[op:T ⟶ T ⟶ T]. ∀[id:T]. ∀[inv:T ⟶ T].
  (<T, eq, le, op, id, inv> ∈ AbMon) supposing (Comm(T;op) and Ident(T;op;id) and Assoc(T;op))
BY
{ ((UnivCD) THENA Auto) }

1
1. T : Type
2. eq : T ⟶ T ⟶ 𝔹
3. le : T ⟶ T ⟶ 𝔹
4. op : T ⟶ T ⟶ T
5. id : T
6. inv : T ⟶ T
7. Assoc(T;op)
8. Ident(T;op;id)
9. Comm(T;op)
⊢ <T, eq, le, op, id, inv> ∈ AbMon

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq,le:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[op:T  {}\mrightarrow{}  T  {}\mrightarrow{}  T].  \mforall{}[id:T].  \mforall{}[inv:T  {}\mrightarrow{}  T].
    (<T,  eq,  le,  op,  id,  inv>  \mmember{}  AbMon)  supposing  (Comm(T;op)  and  Ident(T;op;id)  and  Assoc(T;op))


By

---

Latex:
((UnivCD)  THENA  Auto)

---

Home Index