Nuprl Lemma : vs-lift-bfs-equiv
∀[K:Rng]. ∀[S:Type]. ∀[as,bs:basic-formal-sum(K;S)].
∀[vs:VectorSpace(K)]. ∀[f:S ⟶ Point(vs)]. (vs-lift(vs;f;as) = vs-lift(vs;f;bs) ∈ Point(vs))
supposing bfs-equiv(K;S;as;bs)
Proof
Definitions occuring in Statement :
bfs-equiv: bfs-equiv(K;S;fs1;fs2),
vs-lift: vs-lift(vs;f;fs),
basic-formal-sum: basic-formal-sum(K;S),
vector-space: VectorSpace(K),
vs-point: Point(vs),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
function: x:A ⟶ B[x],
universe: Type,
equal: s = t ∈ T,
rng: Rng
Definitions unfolded in proof :
guard: {T},
prop: ℙ,
all: ∀x:A. B[x],
implies: P ⇒ Q,
basic-formal-sum: basic-formal-sum(K;S),
rng: Rng,
uimplies: b supposing a,
member: t ∈ T,
uall: ∀[x:A]. B[x],
trans: Trans(T;x,y.E[x; y]),
sym: Sym(T;x,y.E[x; y]),
cand: A c∧ B,
refl: Refl(T;x,y.E[x; y]),
and: P ∧ Q,
equiv_rel: EquivRel(T;x,y.E[x; y])
Lemmas referenced :
bfs-equiv_wf,
bfs-reduce_wf,
vs-lift-bfs-reduce,
basic-formal-sum_wf,
vs-lift_wf,
vs-point_wf,
equal_wf,
bfs-equiv-implies
Rules used in proof :
universeEquality,
equalitySymmetry,
equalityTransitivity,
axiomEquality,
isect_memberEquality,
functionEquality,
independent_isectElimination,
sqequalRule,
lambdaFormation,
independent_functionElimination,
applyEquality,
functionExtensionality,
cumulativity,
hypothesis,
rename,
setElimination,
lambdaEquality,
because_Cache,
hypothesisEquality,
thin,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
cut,
introduction,
isect_memberFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
dependent_functionElimination,
independent_pairFormation
Latex:
\mforall{}[K:Rng]. \mforall{}[S:Type]. \mforall{}[as,bs:basic-formal-sum(K;S)].
\mforall{}[vs:VectorSpace(K)]. \mforall{}[f:S {}\mrightarrow{} Point(vs)]. (vs-lift(vs;f;as) = vs-lift(vs;f;bs))
supposing bfs-equiv(K;S;as;bs)
Date html generated:
2018_05_22-PM-09_45_10
Last ObjectModification:
2018_01_09-PM-01_00_25
Theory : linear!algebra
Home
Index