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

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

Proof

Definitions occuring in Statement :  int_seg: `{i..j-}` nat_plus: `ℕ+` bool: `𝔹` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` and: `P ∧ Q` 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 :  weak-continuity-principle-nat+-int-bool-double member: `t ∈ T`
Lemmas referenced :  weak-continuity-principle-nat+-int-bool-double
Rules used in proof :  equalitySymmetry equalityTransitivity sqequalHypSubstitution thin sqequalRule hypothesis extract_by_obid instantiate cut sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution introduction

Latex:
\mforall{}F,H:(\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)  \mwedge{}  H  f  =  H  (G  n))

Date html generated: 2017_09_29-PM-06_06_21
Last ObjectModification: 2017_09_12-PM-02_10_28

Theory : continuity

Home Index