Nuprl Lemma : permutation-ss-sep
∀[rv,f,g,f',g':Top]. (<f, g> # <f', g'> ~ fun-sep(rv;Point;f;f') ∨ fun-sep(rv;Point;g;g'))
Proof
Definitions occuring in Statement :
permutation-ss: permutation-ss(ss),
fun-sep: fun-sep(ss;A;f;g),
ss-sep: x # y,
ss-point: Point,
uall: ∀[x:A]. B[x],
top: Top,
or: P ∨ Q,
pair: <a, b>,
sqequal: s ~ t
Definitions unfolded in proof :
pi2: snd(t),
pi1: fst(t),
prod-ss: ss1 × ss2,
fun-ss: A ⟶ ss,
btrue: tt,
bfalse: ff,
ifthenelse: if b then t else f fi ,
eq_atom: x =a y,
top: Top,
member: t ∈ T,
all: ∀x:A. B[x],
mk-ss: mk-ss,
set-ss: set-ss(ss;x.P[x]),
ss-sep: x # y,
permutation-ss: permutation-ss(ss),
uall: ∀[x:A]. B[x]
Lemmas referenced :
top_wf,
rec_select_update_lemma
Rules used in proof :
because_Cache,
hypothesis,
voidEquality,
voidElimination,
isect_memberEquality,
thin,
dependent_functionElimination,
sqequalHypSubstitution,
extract_by_obid,
introduction,
cut,
sqequalRule,
isect_memberFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}[rv,f,g,f',g':Top]. (<f, g> \# <f', g'> \msim{} fun-sep(rv;Point;f;f') \mvee{} fun-sep(rv;Point;g;g'))
Date html generated:
2016_11_08-AM-09_12_45
Last ObjectModification:
2016_11_03-AM-10_29_28
Theory : inner!product!spaces
Home
Index