Nuprl Lemma : nat-inf-attach-unit

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


Proof




Definitions occuring in Statement :  nat-inf-infinity: nat2inf: n∞ nat-inf: ℕ∞ equipollent: B int_seg: {i..j-} nat: all: x:A. B[x] exists: x:A. B[x] and: P ∧ Q apply: 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 ≥  guard: {T} sq_type: SQType(T) nat: pi1: fst(t) uimplies: supposing a subtype_rel: A ⊆B implies:  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: 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