Nuprl Lemma : non-zero-vector-implies-ext
∀r:RngSig
((∀x,y:|r|. Dec(x = y ∈ |r|)) ⇒ (∀k:ℕ. ∀a:{a:ℕk ⟶ |r|| ¬(a = 0 ∈ (ℕk ⟶ |r|))} . (∃i:ℕk [(¬((a i) = 0 ∈ |r|))])))
Proof
Definitions occuring in Statement :
zero-vector: 0,
int_seg: {i..j-},
nat: ℕ,
decidable: Dec(P),
all: ∀x:A. B[x],
sq_exists: ∃x:A [B[x]],
not: ¬A,
implies: P ⇒ Q,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
natural_number: $n,
equal: s = t ∈ T,
rng_zero: 0,
rng_car: |r|,
rng_sig: RngSig
Definitions unfolded in proof :
so_apply: x[s],
so_lambda: λ2x.t[x],
uimplies: b supposing a,
so_apply: x[s1;s2],
top: Top,
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2;s3;s4],
so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]),
uall: ∀[x:A]. B[x],
decidable__false,
decidable__implies,
any: any x,
decidable__not,
decidable__exists_int_seg,
non-zero-vector-implies,
pi1: fst(t),
ifthenelse: if b then t else f fi ,
genrec-ap: genrec-ap,
it: ⋅,
int_seg_decide: int_seg_decide(d;i;j),
member: t ∈ T
Lemmas referenced :
strict4-decide,
lifting-strict-callbyvalue,
strict4-spread,
lifting-strict-decide,
non-zero-vector-implies,
decidable__false,
decidable__implies,
decidable__not,
decidable__exists_int_seg
Rules used in proof :
independent_isectElimination,
voidEquality,
voidElimination,
isect_memberEquality,
baseClosed,
isectElimination,
equalitySymmetry,
equalityTransitivity,
sqequalHypSubstitution,
thin,
sqequalRule,
hypothesis,
extract_by_obid,
instantiate,
cut,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
introduction
Latex:
\mforall{}r:RngSig
((\mforall{}x,y:|r|. Dec(x = y)) {}\mRightarrow{} (\mforall{}k:\mBbbN{}. \mforall{}a:\{a:\mBbbN{}k {}\mrightarrow{} |r|| \mneg{}(a = 0)\} . (\mexists{}i:\mBbbN{}k [(\mneg{}((a i) = 0))])))
Date html generated:
2018_05_21-PM-09_42_32
Last ObjectModification:
2018_05_20-PM-10_32_56
Theory : matrices
Home
Index