### Nuprl Lemma : equipollent-nat-rationals

`(our proof is constructive so we can compute the listing of rationals`
`       see first-25-rationals)⋅`

`ℕ ~ ℚ`

This theorem is one of freek's list of 100 theorems

Proof

Definitions occuring in Statement :  rationals: `ℚ` equipollent: `A ~ B` nat: `ℕ`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` all: `∀x:A. B[x]` prop: `ℙ` implies: `P `` Q` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` so_lambda: `λ2x.t[x]` so_apply: `x[s]` cand: `A c∧ B` subtract: `n - m` pi2: `snd(t)` cons: `[a / b]` select: `L[n]` le: `A ≤ B` lelt: `i ≤ j < k` int_seg: `{i..j-}` l_exists: `(∃x∈L. P[x])` subtype_rel: `A ⊆r B` exists: `∃x:A. B[x]` satisfiable_int_formula: `satisfiable_int_formula(fmla)` not: `¬A` uimplies: `b supposing a` uiff: `uiff(P;Q)` false: `False` or: `P ∨ Q` decidable: `Dec(P)` guard: `{T}` true: `True` less_than': `less_than'(a;b)` squash: `↓T` less_than: `a < b` nat_plus: `ℕ+` top: `Top` is-qrep: `is-qrep(p)` has-value: `(a)↓` nat: `ℕ` bfalse: `ff` btrue: `tt` ifthenelse: `if b then t else f fi ` sq_type: `SQType(T)` l_member: `(x ∈ l)` ge: `i ≥ j ` int_upper: `{i...}` equipollent: `A ~ B` surject: `Surj(A;B;f)` inject: `Inj(A;B;f)` biject: `Bij(A;B;f)`
Rules used in proof :  cut introduction extract_by_obid sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isectElimination thin hypothesis setEquality productEquality intEquality dependent_functionElimination productElimination independent_pairEquality hypothesisEquality independent_functionElimination sqequalRule lambdaEquality lambdaFormation because_Cache minusEquality imageElimination addEquality applyEquality int_eqEquality dependent_pairFormation approximateComputation independent_isectElimination closedConclusion baseApply promote_hyp pointwiseFunctionality unionElimination rename setElimination applyLambdaEquality equalitySymmetry equalityTransitivity baseClosed imageMemberEquality independent_pairFormation natural_numberEquality dependent_set_memberEquality voidEquality voidElimination isect_memberEquality orFunctionality callbyvalueReduce impliesFunctionality cumulativity instantiate inrFormation inlFormation functionExtensionality

Latex:
\mBbbN{}  \msim{}  \mBbbQ{}

Date html generated: 2018_05_21-PM-11_49_10
Last ObjectModification: 2017_08_09-PM-06_59_20

Theory : rationals

Home Index