### Nuprl Lemma : seq-comp_wf

`∀[T:Type]. ∀[s:sequence(T)]. ∀[B:Type]. ∀[f:T ⟶ B].  (f o s ∈ sequence(B))`

Proof

Definitions occuring in Statement :  seq-comp: `f o s` sequence: `sequence(T)` uall: `∀[x:A]. B[x]` member: `t ∈ T` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` seq-comp: `f o s` sequence: `sequence(T)` nat: `ℕ`
Lemmas referenced :  int_seg_wf sequence_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule spreadEquality sqequalHypSubstitution productElimination thin dependent_pairEquality hypothesisEquality functionEquality extract_by_obid isectElimination natural_numberEquality setElimination rename hypothesis lambdaEquality applyEquality axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality because_Cache universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[s:sequence(T)].  \mforall{}[B:Type].  \mforall{}[f:T  {}\mrightarrow{}  B].    (f  o  s  \mmember{}  sequence(B))

Date html generated: 2018_07_25-PM-01_28_25
Last ObjectModification: 2018_06_11-PM-04_22_14

Theory : arithmetic

Home Index