Nuprl Lemma : basic-continuity
∀[F:(ℤ ⟶ ℤ) ⟶ ℤ]. ∀[f:ℤ ⟶ ℤ].
(↓∃n:ℕ. ∀[g:ℤ ⟶ ℤ]. (F f) = (F g) ∈ ℤ supposing ∀[i:ℤ]. (f i) = (g i) ∈ ℤ supposing |i| < n)
Proof
Definitions occuring in Statement :
absval: |i|,
nat: ℕ,
less_than: a < b,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
exists: ∃x:A. B[x],
squash: ↓T,
apply: f a,
function: x:A ⟶ B[x],
int: ℤ,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
functionEquality,
intEquality,
Continuity,
hypothesisEquality
Latex:
\mforall{}[F:(\mBbbZ{} {}\mrightarrow{} \mBbbZ{}) {}\mrightarrow{} \mBbbZ{}]. \mforall{}[f:\mBbbZ{} {}\mrightarrow{} \mBbbZ{}].
(\mdownarrow{}\mexists{}n:\mBbbN{}. \mforall{}[g:\mBbbZ{} {}\mrightarrow{} \mBbbZ{}]. (F f) = (F g) supposing \mforall{}[i:\mBbbZ{}]. (f i) = (g i) supposing |i| < n)
Date html generated:
2016_05_18-AM-10_49_12
Last ObjectModification:
2015_12_27-PM-10_45_49
Theory : reals
Home
Index