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

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

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



Date html generated: 2017_09_29-PM-06_06_03
Last ObjectModification: 2017_07_08-AM-11_36_19

Theory : continuity


Home Index