Nuprl Lemma : weak-continuity-principle-nat-nat

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

Proof

Definitions occuring in Statement :  int_seg: `{i..j-}` nat: `ℕ` 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` equal: `s = t ∈ T`
Definitions unfolded in proof :  top: `Top` satisfiable_int_formula: `satisfiable_int_formula(fmla)` or: `P ∨ Q` decidable: `Dec(P)` ge: `i ≥ j ` rev_uimplies: `rev_uimplies(P;Q)` uiff: `uiff(P;Q)` guard: `{T}` exists: `∃x:A. B[x]` squash: `↓T` implies: `P `` Q` not: `¬A` false: `False` less_than': `less_than'(a;b)` and: `P ∧ Q` le: `A ≤ B` uimplies: `b supposing a` so_apply: `x[s]` so_lambda: `λ2x.t[x]` subtype_rel: `A ⊆r B` nat: `ℕ` uall: `∀[x:A]. B[x]` prop: `ℙ` member: `t ∈ T` all: `∀x:A. B[x]`
Lemmas referenced :  le_wf int_term_value_constant_lemma int_formula_prop_le_lemma itermConstant_wf intformle_wf decidable__le mu-property assert_wf int_formula_prop_wf int_term_value_var_lemma int_formula_prop_eq_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma itermVar_wf intformeq_wf intformnot_wf intformand_wf full-omega-unsat decidable__equal_int nat_properties assert_of_eq_int eq_int_wf mu_wf and_wf set_wf all_wf exists_wf squash-from-quotient subtype_rel_self false_wf int_seg_subtype_nat subtype_rel_dep_function int_seg_wf equal_wf nat_wf weak-continuity-nat-nat
Rules used in proof :  voidEquality voidElimination isect_memberEquality intEquality int_eqEquality approximateComputation unionElimination applyLambdaEquality equalityTransitivity dependent_set_memberEquality equalitySymmetry levelHypothesis addLevel baseClosed imageMemberEquality dependent_pairFormation productElimination imageElimination independent_functionElimination functionExtensionality independent_pairFormation independent_isectElimination lambdaEquality sqequalRule applyEquality rename setElimination natural_numberEquality isectElimination because_Cache setEquality functionEquality hypothesisEquality thin dependent_functionElimination sqequalHypSubstitution hypothesis lambdaFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution extract_by_obid introduction cut

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

Date html generated: 2017_09_29-PM-06_06_05
Last ObjectModification: 2017_08_30-PM-00_04_43

Theory : continuity

Home Index