### Nuprl Lemma : project-seq_wf

`∀[T:ℕ ⟶ Type]. ∀[n:ℕ]. ∀[s:ℕn ⟶ (i:ℕ × T[i])].  project-seq(s) ∈ i:ℕn ⟶ T[i] supposing ∀i:ℕn. ((fst((s i))) = i ∈ ℤ)`

Proof

Definitions occuring in Statement :  project-seq: `project-seq(s)` int_seg: `{i..j-}` nat: `ℕ` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` so_apply: `x[s]` pi1: `fst(t)` all: `∀x:A. B[x]` member: `t ∈ T` apply: `f a` function: `x:A ⟶ B[x]` product: `x:A × B[x]` natural_number: `\$n` int: `ℤ` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  not: `¬A` false: `False` less_than': `less_than'(a;b)` guard: `{T}` sq_type: `SQType(T)` sq_stable: `SqStable(P)` squash: `↓T` less_than: `a < b` le: `A ≤ B` and: `P ∧ Q` lelt: `i ≤ j < k` int_seg: `{i..j-}` subtype_rel: `A ⊆r B` so_apply: `x[s]` so_lambda: `λ2x.t[x]` nat: `ℕ` pi2: `snd(t)` pi1: `fst(t)` implies: `P `` Q` project-seq: `project-seq(s)` all: `∀x:A. B[x]` uimplies: `b supposing a` member: `t ∈ T` uall: `∀[x:A]. B[x]`
Lemmas referenced :  istype-false int_seg_subtype_nat subtype_rel_self istype-le sq_stable__le subtype_base_sq istype-universe istype-nat less_than_wf and_wf int_subtype_base le_wf set_subtype_base nat_wf pi1_wf istype-int int_seg_wf
Rules used in proof :  independent_pairFormation dependent_set_memberEquality_alt baseClosed imageMemberEquality cumulativity universeEquality instantiate productIsType isectIsTypeImplies isect_memberEquality_alt sqequalBase imageElimination independent_isectElimination intEquality lambdaEquality_alt rename setElimination natural_numberEquality isectElimination extract_by_obid universeIsType functionIsType axiomEquality because_Cache independent_functionElimination equalitySymmetry equalityTransitivity equalityIstype productElimination lambdaFormation_alt hypothesis inhabitedIsType applyEquality sqequalRule hypothesisEquality thin dependent_functionElimination sqequalHypSubstitution functionExtensionality cut introduction isect_memberFormation_alt sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[T:\mBbbN{}  {}\mrightarrow{}  Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[s:\mBbbN{}n  {}\mrightarrow{}  (i:\mBbbN{}  \mtimes{}  T[i])].
project-seq(s)  \mmember{}  i:\mBbbN{}n  {}\mrightarrow{}  T[i]  supposing  \mforall{}i:\mBbbN{}n.  ((fst((s  i)))  =  i)

Date html generated: 2019_10_15-AM-10_20_09
Last ObjectModification: 2019_10_07-PM-04_08_18

Theory : bar-induction

Home Index