Nuprl Lemma : rep-seq-from_wf

[T:Type]. ∀[n:ℕ]. ∀[s:ℕn ⟶ T]. ∀[f:ℕ ⟶ T].  (rep-seq-from(s;n;f) ∈ ℕ ⟶ T)


Proof




Definitions occuring in Statement :  rep-seq-from: rep-seq-from(s;n;f) int_seg: {i..j-} nat: uall: [x:A]. B[x] member: t ∈ T function: x:A ⟶ B[x] natural_number: $n universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T rep-seq-from: rep-seq-from(s;n;f) nat: less_than: a < b and: P ∧ Q less_than': less_than'(a;b) true: True squash: T top: Top not: ¬A implies:  Q false: False prop: int_seg: {i..j-} lelt: i ≤ j < k
Lemmas referenced :  less_than_wf int_seg_wf lelt_wf nat_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lambdaEquality sqequalHypSubstitution setElimination thin rename because_Cache hypothesis lessCases independent_pairFormation isectElimination baseClosed natural_numberEquality equalityTransitivity equalitySymmetry imageMemberEquality hypothesisEquality axiomSqEquality isect_memberEquality voidElimination voidEquality lambdaFormation imageElimination productElimination extract_by_obid independent_functionElimination applyEquality functionExtensionality dependent_set_memberEquality axiomEquality functionEquality universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[s:\mBbbN{}n  {}\mrightarrow{}  T].  \mforall{}[f:\mBbbN{}  {}\mrightarrow{}  T].    (rep-seq-from(s;n;f)  \mmember{}  \mBbbN{}  {}\mrightarrow{}  T)



Date html generated: 2019_06_20-PM-02_56_52
Last ObjectModification: 2018_08_20-PM-09_38_45

Theory : continuity


Home Index