### Nuprl Lemma : mon_for_wf

`∀g:IMonoid. ∀A:Type. ∀as:A List. ∀f:A ⟶ |g|.  (For{g} x ∈ as. f[x] ∈ |g|)`

Proof

Definitions occuring in Statement :  mon_for: `For{g} x ∈ as. f[x]` list: `T List` so_apply: `x[s]` all: `∀x:A. B[x]` member: `t ∈ T` function: `x:A ⟶ B[x]` universe: `Type` imon: `IMonoid` grp_car: `|g|`
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` mon_for: `For{g} x ∈ as. f[x]` uall: `∀[x:A]. B[x]` imon: `IMonoid` so_lambda: `λ2x.t[x]` so_apply: `x[s]`
Lemmas referenced :  for_wf grp_car_wf grp_op_wf grp_id_wf istype-universe list_wf imon_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt cut sqequalRule introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality setElimination rename because_Cache hypothesis lambdaEquality_alt applyEquality functionIsType universeIsType universeEquality

Latex:
\mforall{}g:IMonoid.  \mforall{}A:Type.  \mforall{}as:A  List.  \mforall{}f:A  {}\mrightarrow{}  |g|.    (For\{g\}  x  \mmember{}  as.  f[x]  \mmember{}  |g|)

Date html generated: 2019_10_16-PM-01_02_18
Last ObjectModification: 2018_10_08-AM-11_49_28

Theory : list_2

Home Index