### 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