Nuprl Lemma : sign-flip
∀[n:ℕ]. ∀[u,v:ℕn]. permutation-sign(n;(u, v)) = (-1) ∈ ℤ supposing ¬(u = v ∈ ℤ)
Proof
Definitions occuring in Statement :
permutation-sign: permutation-sign(n;f),
flip: (i, j),
int_seg: {i..j-},
nat: ℕ,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
not: ¬A,
minus: -n,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Definitions unfolded in proof :
int_seg: {i..j-},
subtype_rel: A ⊆r B,
true: True,
compose: f o g,
squash: ↓T,
uimplies: b supposing a,
prop: ℙ,
nat: ℕ,
member: t ∈ T,
uall: ∀[x:A]. B[x]
Lemmas referenced :
not_wf,
permutation-sign-id,
int_subtype_base,
equal-wf-base,
flip_wf,
nat_wf,
permutation-sign_wf,
true_wf,
squash_wf,
equal_wf,
inject_wf,
int_seg_wf,
identity-injection,
permutation-sign-flip
Rules used in proof :
minusEquality,
closedConclusion,
baseApply,
setEquality,
baseClosed,
imageMemberEquality,
functionEquality,
intEquality,
universeEquality,
equalityTransitivity,
imageElimination,
sqequalRule,
equalitySymmetry,
hyp_replacement,
independent_isectElimination,
applyEquality,
functionExtensionality,
because_Cache,
lambdaEquality,
dependent_set_memberEquality,
rename,
setElimination,
natural_numberEquality,
hypothesisEquality,
thin,
isectElimination,
sqequalHypSubstitution,
hypothesis,
isect_memberFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
extract_by_obid,
introduction,
cut
Latex:
\mforall{}[n:\mBbbN{}]. \mforall{}[u,v:\mBbbN{}n]. permutation-sign(n;(u, v)) = (-1) supposing \mneg{}(u = v)
Date html generated:
2018_05_21-PM-00_59_01
Last ObjectModification:
2017_12_10-PM-11_26_58
Theory : num_thy_1
Home
Index