Nuprl Lemma : Degree-implies-BrowerFPT-ext
∀n:ℕ. BrouwerFPT(n + 1) supposing ¬¬DegreeExists(n)
Proof
Definitions occuring in Statement :
DegreeExists: DegreeExists(n),
BrouwerFPT: BrouwerFPT(n),
nat: ℕ,
uimplies: b supposing a,
all: ∀x:A. B[x],
not: ¬A,
add: n + m,
natural_number: $n
Definitions unfolded in proof :
member: t ∈ T,
Degree-implies-BrowerFPT,
NoBallRetraction-implies-BrouwerFPT,
approx-fixpoint-unit-ball-2
Lemmas referenced :
Degree-implies-BrowerFPT,
NoBallRetraction-implies-BrouwerFPT,
approx-fixpoint-unit-ball-2
Rules used in proof :
introduction,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
cut,
instantiate,
extract_by_obid,
hypothesis,
sqequalRule,
thin,
sqequalHypSubstitution,
equalityTransitivity,
equalitySymmetry
Latex:
\mforall{}n:\mBbbN{}. BrouwerFPT(n + 1) supposing \mneg{}\mneg{}DegreeExists(n)
Date html generated:
2019_10_30-AM-11_30_20
Last ObjectModification:
2019_08_06-PM-01_44_53
Theory : real!vectors
Home
Index