Step
*
of Lemma
mk_abdmonoid
∀[T:Type]. ∀[eq,le:T ⟶ T ⟶ 𝔹]. ∀[op:T ⟶ T ⟶ T]. ∀[id:T]. ∀[inv:T ⟶ T].
(<T, eq, le, op, id, inv> ∈ AbDMon) supposing (Comm(T;op) and Ident(T;op;id) and Assoc(T;op) and IsEqFun(T;eq))
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. IsEqFun(T;eq)
8. Assoc(T;op)
9. Ident(T;op;id)
10. Comm(T;op)
⊢ <T, eq, le, op, id, inv> ∈ AbDMon
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{} AbDMon) supposing
(Comm(T;op) and
Ident(T;op;id) and
Assoc(T;op) and
IsEqFun(T;eq))
By
Latex:
((UnivCD) THENA Auto)
Home
Index