Nuprl Lemma : permutation-ss-eq
∀[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-eq: x ≡ y,
ss-point: Point,
uall: ∀[x:A]. B[x],
top: Top,
not: ¬A,
or: P ∨ Q,
pair: <a, b>,
sqequal: s ~ t
Definitions unfolded in proof :
member: t ∈ T,
ss-eq: x ≡ y,
uall: ∀[x:A]. B[x]
Lemmas referenced :
top_wf,
permutation-ss-sep
Rules used in proof :
because_Cache,
hypothesis,
hypothesisEquality,
thin,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
introduction,
cut,
sqequalRule,
isect_memberFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}[rv,f,g,f',g':Top]. (<f, g> \mequiv{} <f', g'> \msim{} \mneg{}(fun-sep(rv;Point;f;f') \mvee{} fun-sep(rv;Point;g;g')))
Date html generated:
2016_11_08-AM-09_12_47
Last ObjectModification:
2016_11_03-AM-10_29_41
Theory : inner!product!spaces
Home
Index