### Nuprl Lemma : strong-continuity2-implies-weak

F:(ℕ ⟶ ℕ) ⟶ ℕ. ∀f:ℕ ⟶ ℕ.  ⇃(∃n:ℕ. ∀g:ℕ ⟶ ℕ((f g ∈ (ℕn ⟶ ℕ))  ((F f) (F g) ∈ ℕ)))

Proof

Definitions occuring in Statement :  quotient: x,y:A//B[x; y] int_seg: {i..j-} nat: all: x:A. B[x] exists: x:A. B[x] implies:  Q true: True apply: a function: x:A ⟶ B[x] natural_number: \$n equal: t ∈ T
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T uall: [x:A]. B[x] prop: exists: x:A. B[x] implies:  Q subtype_rel: A ⊆B nat: uimplies: supposing a le: A ≤ B and: P ∧ Q less_than': less_than'(a;b) false: False not: ¬A so_lambda: λ2x.t[x] so_apply: x[s] guard: {T} decidable: Dec(P) or: P ∨ Q ge: i ≥  satisfiable_int_formula: satisfiable_int_formula(fmla) top: Top
Lemmas referenced :  istype-nat strong-continuity2-implies-weak-skolem implies-quotient-true nat_wf equal_wf int_seg_wf subtype_rel_function int_seg_subtype_nat istype-false subtype_rel_self equal-wf-base set_subtype_base le_wf istype-int int_subtype_base decidable__le nat_properties full-omega-unsat intformand_wf intformle_wf itermConstant_wf itermVar_wf intformnot_wf int_formula_prop_and_lemma istype-void int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_not_lemma int_formula_prop_wf istype-le
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :lambdaFormation_alt,  Error :functionIsType,  cut introduction extract_by_obid hypothesis because_Cache Error :inhabitedIsType,  hypothesisEquality sqequalHypSubstitution dependent_functionElimination thin isectElimination sqequalRule productEquality functionEquality natural_numberEquality applyEquality Error :lambdaEquality_alt,  setElimination rename independent_isectElimination independent_pairFormation intEquality closedConclusion independent_functionElimination productElimination Error :productIsType,  Error :equalityIsType1,  Error :universeIsType,  Error :equalityIsType4,  Error :dependent_pairFormation_alt,  unionElimination equalityTransitivity equalitySymmetry applyLambdaEquality approximateComputation int_eqEquality Error :isect_memberEquality_alt,  voidElimination Error :dependent_set_memberEquality_alt

Latex:
\mforall{}F:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.    \00D9(\mexists{}n:\mBbbN{}.  \mforall{}g:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  ((f  =  g)  {}\mRightarrow{}  ((F  f)  =  (F  g))))

Date html generated: 2019_06_20-PM-02_51_45
Last ObjectModification: 2018_11_21-AM-09_56_24

Theory : continuity

Home Index