### Nuprl Lemma : weak-continuity-principle-nat+-int-bool-ext

`∀F:(ℕ+ ⟶ ℤ) ⟶ 𝔹. ∀f:ℕ+ ⟶ ℤ. ∀G:n:ℕ+ ⟶ {g:ℕ+ ⟶ ℤ| f = g ∈ (ℕ+n ⟶ ℤ)} .  ∃n:ℕ+. F f = F (G n)`

Proof

Definitions occuring in Statement :  int_seg: `{i..j-}` nat_plus: `ℕ+` bool: `𝔹` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` set: `{x:A| B[x]} ` apply: `f a` function: `x:A ⟶ B[x]` natural_number: `\$n` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  member: `t ∈ T` weak-continuity-principle-nat+-int-bool
Lemmas referenced :  weak-continuity-principle-nat+-int-bool
Rules used in proof :  introduction sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut instantiate extract_by_obid hypothesis sqequalRule thin sqequalHypSubstitution equalityTransitivity equalitySymmetry

Latex:
\mforall{}F:(\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{})  {}\mrightarrow{}  \mBbbB{}.  \mforall{}f:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}.  \mforall{}G:n:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \{g:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}|  f  =  g\}  .    \mexists{}n:\mBbbN{}\msupplus{}.  F  f  =  F  (G  n)

Date html generated: 2017_09_29-PM-06_06_13
Last ObjectModification: 2017_07_08-PM-00_16_07

Theory : continuity

Home Index