### Nuprl Lemma : reals-uncountable-simple

`∀f:ℕ ⟶ ℝ. (¬Surj(ℕ;ℝ;f))`

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

Proof

Definitions occuring in Statement :  real: `ℝ` surject: `Surj(A;B;f)` nat: `ℕ` all: `∀x:A. B[x]` not: `¬A` function: `x:A ⟶ B[x]`
Definitions unfolded in proof :  all: `∀x:A. B[x]` not: `¬A` implies: `P `` Q` false: `False` member: `t ∈ T` uall: `∀[x:A]. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` less_than: `a < b` squash: `↓T` less_than': `less_than'(a;b)` true: `True` exists: `∃x:A. B[x]` prop: `ℙ` surject: `Surj(A;B;f)` subtype_rel: `A ⊆r B` uimplies: `b supposing a` guard: `{T}`
Lemmas referenced :  rneq_irreflexivity iff_weakening_equal true_wf squash_wf rneq_wf real_wf nat_wf surject_wf rless-int int-to-real_wf reals-uncountable
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut thin lemma_by_obid sqequalHypSubstitution dependent_functionElimination hypothesisEquality isectElimination natural_numberEquality hypothesis independent_functionElimination productElimination sqequalRule independent_pairFormation introduction imageMemberEquality baseClosed because_Cache voidElimination functionEquality applyEquality lambdaEquality imageElimination equalityTransitivity equalitySymmetry universeEquality independent_isectElimination

Latex:
\mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}.  (\mneg{}Surj(\mBbbN{};\mBbbR{};f))

Date html generated: 2016_05_18-AM-07_56_34
Last ObjectModification: 2016_01_17-AM-02_16_44

Theory : reals

Home Index