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: supposing a uall: [x:A]. B[x] exists: x:A. B[x] squash: T apply: a function: x:A ⟶ B[x] int: equal: 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