Step
*
1
of Lemma
free_abmon_endomorph_is_id
1. S : DSet
2. M : FAbMon(S)
3. f : MonHom(M.mon,M.mon)
4. (f o M.inj) = M.inj ∈ (|S| ⟶ |M.mon|)
⊢ f = Id{|M.mon|} ∈ (|M.mon| ⟶ |M.mon|)
BY
{ % Should be nicer way to get this...%
((InstLemma `free_abmon_umap_properties`
[S;M;M.mon;M.inj]
THENM D (-1)) THENA Auto) }
1
1. S : DSet
2. M : FAbMon(S)
3. f : MonHom(M.mon,M.mon)
4. (f o M.inj) = M.inj ∈ (|S| ⟶ |M.mon|)
5. ((M.umap M.mon M.inj) o M.inj) = M.inj ∈ (|S| ⟶ |M.mon|)
6. ∀f:MonHom(M.mon,M.mon)
(((f o M.inj) = M.inj ∈ (|S| ⟶ |M.mon|))
⇒ (f = (M.umap M.mon M.inj) ∈ (|M.mon| ⟶ |M.mon|)))
⊢ f = Id{|M.mon|} ∈ (|M.mon| ⟶ |M.mon|)
Latex:
Latex:
1. S : DSet
2. M : FAbMon(S)
3. f : MonHom(M.mon,M.mon)
4. (f o M.inj) = M.inj
\mvdash{} f = Id\{|M.mon|\}
By
Latex:
\% Should be nicer way to get this...\%
((InstLemma `free\_abmon\_umap\_properties`
[S;M;M.mon;M.inj]
THENM D (-1)) THENA Auto)
Home
Index