Nuprl Lemma : weak-continuity-nat-nat
∀F:(ℕ ⟶ ℕ) ⟶ ℕ. ∀f:ℕ ⟶ ℕ. ⇃(∃n:ℕ. ∀g:ℕ ⟶ ℕ. ((f = g ∈ (ℕn ⟶ ℕ)) ⇒ ((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
Lemmas referenced :
strong-continuity2-implies-weak
Rules used in proof :
hypothesis,
extract_by_obid,
introduction,
cut
Latex:
\mforall{}F:(\mBbbN{} {}\mrightarrow{} \mBbbN{}) {}\mrightarrow{} \mBbbN{}. \mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbN{}. \00D9(\mexists{}n:\mBbbN{}. \mforall{}g:\mBbbN{} {}\mrightarrow{} \mBbbN{}. ((f = g) {}\mRightarrow{} ((F f) = (F g))))
Date html generated:
2017_09_29-PM-06_05_59
Last ObjectModification:
2017_08_30-PM-00_01_53
Theory : continuity
Home
Index