Nuprl Lemma : weak-continuity-nat-int
∀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,
int: ℤ,
equal: s = t ∈ T
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
implies: P ⇒ Q
Lemmas referenced :
weak-continuity-equipollent,
equipollent-int-nat
Rules used in proof :
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
dependent_functionElimination,
thin,
intEquality,
independent_functionElimination,
hypothesis
Latex:
\mforall{}F:(\mBbbN{} {}\mrightarrow{} \mBbbZ{}) {}\mrightarrow{} \mBbbN{}. \mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbZ{}. \00D9(\mexists{}n:\mBbbN{}. \mforall{}g:\mBbbN{} {}\mrightarrow{} \mBbbZ{}. ((f = g) {}\mRightarrow{} ((F f) = (F g))))
Date html generated:
2017_09_29-PM-06_05_58
Last ObjectModification:
2017_07_05-PM-06_15_58
Theory : continuity
Home
Index