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