### Nuprl Lemma : nat-inf-attach-unit

`∀F:ℕ ⟶ Type. ∃G:ℕ∞ ⟶ Type. ((∀n:ℕ. G n∞ ~ F n) ∧ G ∞ ~ ℕ1)`

Proof

Definitions occuring in Statement :  nat-inf-infinity: `∞` nat2inf: `n∞` nat-inf: `ℕ∞` equipollent: `A ~ B` int_seg: `{i..j-}` nat: `ℕ` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` and: `P ∧ Q` apply: `f a` function: `x:A ⟶ B[x]` natural_number: `\$n` universe: `Type`
Definitions unfolded in proof :  top: `Top` false: `False` satisfiable_int_formula: `satisfiable_int_formula(fmla)` not: `¬A` or: `P ∨ Q` decidable: `Dec(P)` ge: `i ≥ j ` guard: `{T}` sq_type: `SQType(T)` nat: `ℕ` pi1: `fst(t)` uimplies: `b supposing a` subtype_rel: `A ⊆r B` implies: `P `` Q` singleton-type: `singleton-type(A)` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` member: `t ∈ T` uall: `∀[x:A]. B[x]` prop: `ℙ` and: `P ∧ Q` cand: `A c∧ B` so_lambda: `λ2x.t[x]` so_apply: `x[s]`
Lemmas referenced :  nat-inf-infinity-new equal-wf-base-T equipollent-empty-domain int_formula_prop_wf int_term_value_var_lemma int_formula_prop_eq_lemma int_formula_prop_not_lemma itermVar_wf intformeq_wf intformnot_wf full-omega-unsat decidable__equal_int nat_properties le_wf set_subtype_base int_subtype_base subtype_base_sq subtype_rel_self subtype_rel_dep_function equipollent-singleton-domain set_wf nat2inf-one-one nat_wf equal_wf nat-inf_wf nat2inf_wf all_wf equipollent_wf nat-inf-infinity_wf int_seg_wf
Rules used in proof :  baseClosed voidEquality voidElimination isect_memberEquality int_eqEquality approximateComputation unionElimination equalityTransitivity productElimination intEquality independent_isectElimination instantiate dependent_functionElimination equalitySymmetry independent_functionElimination because_Cache dependent_set_memberEquality sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation dependent_pairFormation lambdaEquality functionEquality setEquality cut introduction extract_by_obid hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality applyEquality functionExtensionality setElimination rename independent_pairFormation productEquality sqequalRule natural_numberEquality cumulativity universeEquality

Latex:
\mforall{}F:\mBbbN{}  {}\mrightarrow{}  Type.  \mexists{}G:\mBbbN{}\minfty{}  {}\mrightarrow{}  Type.  ((\mforall{}n:\mBbbN{}.  G  n\minfty{}  \msim{}  F  n)  \mwedge{}  G  \minfty{}  \msim{}  \mBbbN{}1)

Date html generated: 2018_07_29-AM-09_29_18
Last ObjectModification: 2018_07_27-PM-05_28_45

Theory : basic

Home Index