Nuprl Lemma : strong-continuity2-implies-weak-skolem
∀F:(ℕ ⟶ ℕ) ⟶ ℕ. ⇃(∃M:(ℕ ⟶ ℕ) ⟶ ℕ. ∀f,g:ℕ ⟶ ℕ. ((f = g ∈ (ℕM f ⟶ ℕ)) ⇒ ((F f) = (F g) ∈ ℕ)))
Proof
Definitions occuring in Statement :
quotient: x,y:A//B[x; y],
int_seg: {i..j-},
nat: ℕ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
true: True,
apply: f a,
function: x:A ⟶ B[x],
natural_number: $n,
equal: s = t ∈ T
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
strong-continuity2: strong-continuity2(T;F),
weak-continuity-skolem: weak-continuity-skolem(T;F),
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
prop: ℙ,
guard: {T}
Lemmas referenced :
strong-continuity2-no-inner-squash,
implies-quotient-true,
strong-continuity2_wf,
nat_wf,
weak-continuity-skolem_wf,
strong-continuity2-weak-skolem
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
hypothesisEquality,
hypothesis,
isectElimination,
functionExtensionality,
applyEquality,
functionEquality,
independent_functionElimination,
because_Cache
Latex:
\mforall{}F:(\mBbbN{} {}\mrightarrow{} \mBbbN{}) {}\mrightarrow{} \mBbbN{}. \00D9(\mexists{}M:(\mBbbN{} {}\mrightarrow{} \mBbbN{}) {}\mrightarrow{} \mBbbN{}. \mforall{}f,g:\mBbbN{} {}\mrightarrow{} \mBbbN{}. ((f = g) {}\mRightarrow{} ((F f) = (F g))))
Date html generated:
2016_12_12-AM-09_23_24
Last ObjectModification:
2016_11_22-PM-00_07_27
Theory : continuity
Home
Index