Nuprl Lemma : power-vs-sq
∀[K,S:Top]. (K^S ~ Point= S ⟶ |K| zero= λs.0 a+b= λs.((a s) +K (b s)) a*b= λs.(a * (b s)))
Proof
Definitions occuring in Statement :
power-vs: K^S,
mk-vs: mk-vs,
uall: ∀[x:A]. B[x],
top: Top,
infix_ap: x f y,
apply: f a,
lambda: λx.A[x],
function: x:A ⟶ B[x],
sqequal: s ~ t,
rng_times: *,
rng_zero: 0,
rng_plus: +r,
rng_car: |r|
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
power-vs: K^S,
vs-exp: V^S,
vs-sum: Σs:S. V[s],
one-dim-vs: one-dim-vs(K),
vs-point: Point(vs),
mk-vs: mk-vs,
all: ∀x:A. B[x],
top: Top,
eq_atom: x =a y,
ifthenelse: if b then t else f fi ,
bfalse: ff,
btrue: tt,
vs-0: 0,
vs-add: x + y,
vs-mul: a * x
Lemmas referenced :
rec_select_update_lemma,
top_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
sqequalRule,
extract_by_obid,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
isect_memberEquality,
voidElimination,
voidEquality,
hypothesis,
sqequalAxiom,
isectElimination,
hypothesisEquality,
because_Cache
Latex:
\mforall{}[K,S:Top]. (K\^{}S \msim{} Point= S {}\mrightarrow{} |K| zero= \mlambda{}s.0 a+b= \mlambda{}s.((a s) +K (b s)) a*b= \mlambda{}s.(a * (b s)))
Date html generated:
2018_05_22-PM-09_42_41
Last ObjectModification:
2017_11_09-PM-01_42_29
Theory : linear!algebra
Home
Index