### Nuprl Lemma : nat-inf-attach

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

Proof

Definitions occuring in Statement :  nat-inf-infinity: `∞` nat2inf: `n∞` nat-inf: `ℕ∞` equipollent: `A ~ B` nat: `ℕ` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` and: `P ∧ Q` apply: `f a` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  nat: `ℕ` le: `A ≤ B` less_than': `less_than'(a;b)` false: `False` not: `¬A` int-prod: `Π(f[x] | x < k)` top: `Top` cand: `A c∧ B` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` implies: `P `` Q` uimplies: `b supposing a` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` all: `∀x:A. B[x]` member: `t ∈ T` uall: `∀[x:A]. B[x]` exists: `∃x:A. B[x]` and: `P ∧ Q`
Lemmas referenced :  nat_wf int_seg_wf nat-inf-attach-unit ext-eq_weakening equipollent_weakening_ext-eq function_functionality_wrt_equipollent_left equipollent_functionality_wrt_equipollent equipollent-void-domain nat-inf-infinity_wf nat2inf_wf equipollent_wf all_wf and_wf nat-inf_wf equipollent-product primrec1_lemma le_wf false_wf int-prod_wf product_functionality_wrt_equipollent_right product_functionality_wrt_equipollent equipollent-multiply equipollent-product-one union_functionality_wrt_equipollent equipollent-product-zero equipollent-sum-zero
Rules used in proof :  multiplyEquality addLevel allFunctionality levelHypothesis andLevelFunctionality allLevelFunctionality unionEquality productEquality dependent_set_memberEquality isect_memberEquality voidElimination voidEquality dependent_pairFormation applyEquality hypothesisEquality independent_pairFormation because_Cache independent_functionElimination independent_isectElimination sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut lemma_by_obid sqequalHypSubstitution dependent_functionElimination thin lambdaEquality isectElimination natural_numberEquality hypothesis productElimination sqequalRule rename universeEquality functionEquality cumulativity

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

Date html generated: 2018_07_29-AM-09_29_23
Last ObjectModification: 2018_07_27-PM-05_34_13

Theory : basic

Home Index