Nuprl Lemma : oal_umap_char_a
∀s:LOSet. ∀g:AbDMon. ∀h:AbMon. ∀f:|s| ⟶ MonHom(g,h).
umap(h,f) = !v:|oal(s;g)| ⟶ |h|
(IsMonHom{oal_mon(s;g),h}(v) ∧ (∀j:|s|. ((f j) = (v o (λw.inj(j,w))) ∈ (|g| ⟶ |h|))))
Proof
Definitions occuring in Statement :
oal_umap: umap(h,f),
oal_inj: inj(k,v),
oal_mon: oal_mon(a;b),
oalist: oal(a;b),
compose: f o g,
uni_sat: a = !x:T. Q[x],
all: ∀x:A. B[x],
and: P ∧ Q,
apply: f a,
lambda: λx.A[x],
function: x:A ⟶ B[x],
equal: s = t ∈ T,
monoid_hom: MonHom(M1,M2),
monoid_hom_p: IsMonHom{M1,M2}(f),
abdmonoid: AbDMon,
abmonoid: AbMon,
grp_car: |g|,
loset: LOSet,
set_car: |p|
Definitions unfolded in proof :
oal_umap: umap(h,f)
Lemmas referenced :
oal_umap_char
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
lemma_by_obid
Latex:
\mforall{}s:LOSet. \mforall{}g:AbDMon. \mforall{}h:AbMon. \mforall{}f:|s| {}\mrightarrow{} MonHom(g,h).
umap(h,f) = !v:|oal(s;g)| {}\mrightarrow{} |h|
(IsMonHom\{oal\_mon(s;g),h\}(v) \mwedge{} (\mforall{}j:|s|. ((f j) = (v o (\mlambda{}w.inj(j,w))))))
Date html generated:
2016_05_16-AM-08_22_59
Last ObjectModification:
2015_12_28-PM-06_24_48
Theory : polynom_2
Home
Index