### Nuprl Lemma : WCPD_wf

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

Proof

Definitions occuring in Statement :  WCPD: `WCPD(F;H;f;G)` int_seg: `{i..j-}` nat_plus: `ℕ+` bool: `𝔹` all: `∀x:A. B[x]` and: `P ∧ Q` member: `t ∈ T` 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 :  WCPD: `WCPD(F;H;f;G)` weak-continuity-principle-nat+-int-bool-double-ext pi1: `fst(t)` prop: `ℙ` implies: `P `` Q` not: `¬A` false: `False` less_than': `less_than'(a;b)` le: `A ≤ B` uimplies: `b supposing a` so_apply: `x[s]` nat_plus: `ℕ+` so_lambda: `λ2x.t[x]` uall: `∀[x:A]. B[x]` subtype_rel: `A ⊆r B` exists: `∃x:A. B[x]` and: `P ∧ Q` member: `t ∈ T` all: `∀x:A. B[x]`
Lemmas referenced :  set_wf bool_wf exists_wf subtype_rel_self false_wf int_seg_subtype_nat_plus nat_plus_wf subtype_rel_dep_function int_seg_wf equal_wf all_wf weak-continuity-principle-nat+-int-bool-double-ext
Rules used in proof :  independent_functionElimination dependent_functionElimination equalitySymmetry equalityTransitivity dependent_set_memberEquality productElimination productEquality independent_pairFormation independent_isectElimination intEquality rename setElimination natural_numberEquality setEquality functionEquality isectElimination introduction lambdaEquality because_Cache hypothesisEquality sqequalHypSubstitution sqequalRule functionExtensionality applyEquality hypothesis extract_by_obid instantiate thin cut lambdaFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

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\}  .
(WCPD(F;H;f;G)  \mmember{}  \{n:\mBbbN{}\msupplus{}|  F  f  =  F  (G  n)  \mwedge{}  H  f  =  H  (G  n)\}  )

Date html generated: 2017_09_29-PM-06_06_33
Last ObjectModification: 2017_09_12-PM-02_15_31

Theory : continuity

Home Index