Nuprl Lemma : seq-settype
∀[T:Type]. ∀[P:T ⟶ ℙ]. ∀[s:sequence(T)]. s ∈ sequence({x:T| P[x]} ) supposing ∀i:ℕ||s||. (↓P[s[i]])
Proof
Definitions occuring in Statement :
seq-item: s[i],
seq-len: ||s||,
sequence: sequence(T),
int_seg: {i..j-},
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
prop: ℙ,
so_apply: x[s],
all: ∀x:A. B[x],
squash: ↓T,
member: t ∈ T,
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
natural_number: $n,
universe: Type
Definitions unfolded in proof :
all: ∀x:A. B[x],
guard: {T},
squash: ↓T,
so_lambda: λ2x.t[x],
prop: ℙ,
subtype_rel: A ⊆r B,
so_apply: x[s],
nat: ℕ,
pi2: snd(t),
pi1: fst(t),
seq-len: ||s||,
seq-item: s[i],
sequence: sequence(T),
uimplies: b supposing a,
member: t ∈ T,
uall: ∀[x:A]. B[x]
Lemmas referenced :
sequence_wf,
seq-item_wf,
squash_wf,
nat_wf,
seq-len_wf,
all_wf,
subtype_rel_self,
int_seg_wf
Rules used in proof :
dependent_functionElimination,
dependent_set_memberEquality,
imageElimination,
universeEquality,
isect_memberEquality,
lambdaEquality,
equalitySymmetry,
equalityTransitivity,
axiomEquality,
instantiate,
applyEquality,
cumulativity,
setEquality,
functionEquality,
hypothesis,
because_Cache,
rename,
setElimination,
natural_numberEquality,
isectElimination,
extract_by_obid,
functionExtensionality,
hypothesisEquality,
dependent_pairEquality,
sqequalRule,
thin,
productElimination,
sqequalHypSubstitution,
cut,
introduction,
isect_memberFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}[T:Type]. \mforall{}[P:T {}\mrightarrow{} \mBbbP{}]. \mforall{}[s:sequence(T)]. s \mmember{} sequence(\{x:T| P[x]\} ) supposing \mforall{}i:\mBbbN{}||s||. (\mdownarrow{}P[s[i]]\000C)
Date html generated:
2018_07_25-PM-01_29_31
Last ObjectModification:
2018_06_18-PM-06_55_01
Theory : arithmetic
Home
Index