Nuprl Lemma : markov-streamless-iff
(∀P:ℕ ⟶ ℙ. ((∀m:ℕ. ((P m) ∨ (¬(P m)))) ⇒ (¬(∀m:ℕ. (¬(P m)))) ⇒ (∃m:ℕ. (P m))))
⇒ (∀T:Type. (streamless(T) ⇐⇒ (∀x,y:T. Dec(x = y ∈ T)) ∧ (¬¬(∃n:ℕ. T ~ ℕn))))
Proof
Definitions occuring in Statement :
streamless: streamless(T),
equipollent: A ~ B,
int_seg: {i..j-},
nat: ℕ,
decidable: Dec(P),
prop: ℙ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
iff: P ⇐⇒ Q,
not: ¬A,
implies: P ⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
apply: f a,
function: x:A ⟶ B[x],
natural_number: $n,
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
implies: P ⇒ Q,
all: ∀x:A. B[x],
member: t ∈ T,
prop: ℙ,
uall: ∀[x:A]. B[x],
subtype_rel: A ⊆r B,
so_lambda: λ2x.t[x],
so_apply: x[s],
iff: P ⇐⇒ Q,
and: P ∧ Q,
not: ¬A,
false: False,
nat: ℕ,
exists: ∃x:A. B[x],
rev_implies: P ⇐ Q,
cand: A c∧ B,
guard: {T}
Lemmas referenced :
all_wf,
nat_wf,
or_wf,
not_wf,
exists_wf,
list_wf,
no_repeats_wf,
equal_wf,
length_wf,
l_member_wf,
decidable_wf,
equipollent_wf,
int_seg_wf,
streamless_wf,
iff_wf,
markov-streamless-iff-not-not-enum,
equipollent-iff-list,
deq-exists,
length_wf_nat,
remove-repeats_wf,
remove-repeats-no_repeats,
remove-repeats_property
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
universeEquality,
cut,
instantiate,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
functionEquality,
hypothesis,
applyEquality,
lambdaEquality,
cumulativity,
hypothesisEquality,
sqequalRule,
functionExtensionality,
because_Cache,
independent_pairFormation,
productElimination,
dependent_functionElimination,
independent_functionElimination,
voidElimination,
productEquality,
intEquality,
setElimination,
rename,
dependent_pairFormation,
natural_numberEquality,
addLevel,
impliesFunctionality,
existsFunctionality,
existsLevelFunctionality,
impliesLevelFunctionality,
andLevelFunctionality
Latex:
(\mforall{}P:\mBbbN{} {}\mrightarrow{} \mBbbP{}. ((\mforall{}m:\mBbbN{}. ((P m) \mvee{} (\mneg{}(P m)))) {}\mRightarrow{} (\mneg{}(\mforall{}m:\mBbbN{}. (\mneg{}(P m)))) {}\mRightarrow{} (\mexists{}m:\mBbbN{}. (P m))))
{}\mRightarrow{} (\mforall{}T:Type. (streamless(T) \mLeftarrow{}{}\mRightarrow{} (\mforall{}x,y:T. Dec(x = y)) \mwedge{} (\mneg{}\mneg{}(\mexists{}n:\mBbbN{}. T \msim{} \mBbbN{}n))))
Date html generated:
2018_05_21-PM-09_03_16
Last ObjectModification:
2017_07_26-PM-06_26_06
Theory : general
Home
Index