Nuprl Lemma : reals-uncountable-simple

f:ℕ ⟶ ℝSurj(ℕ;ℝ;f))

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


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:  Q false: False member: t ∈ T uall: [x:A]. B[x] iff: ⇐⇒ Q and: P ∧ Q rev_implies:  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 ⊆B uimplies: 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

\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