Nuprl Lemma : dfan-implies-twkl!
∀[T:Type]. ((∃size:ℕ. T ~ ℕsize) ⇒ Fan_d(T) ⇒ WKL!(T))
Proof
Definitions occuring in Statement :
twkl!: WKL!(T),
dfan: Fan_d(T),
equipollent: A ~ B,
int_seg: {i..j-},
nat: ℕ,
uall: ∀[x:A]. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
natural_number: $n,
universe: Type
Definitions unfolded in proof :
nat: ℕ,
exists: ∃x:A. B[x],
prop: ℙ,
subtype_rel: A ⊆r B,
and: P ∧ Q,
false: False,
not: ¬A,
all: ∀x:A. B[x],
implies: P ⇒ Q,
member: t ∈ T,
uall: ∀[x:A]. B[x]
Lemmas referenced :
fan-implies-barred-not-unbounded,
fan-implies-bar-sep,
istype-universe,
int_seg_wf,
equipollent_wf,
istype-nat,
dfan_wf,
dbar_wf,
unbounded-list-predicate_wf,
subtype_rel_self,
list_wf,
predicate-not_wf,
down-closed_wf,
bar-separation-implies-twkl!
Rules used in proof :
dependent_functionElimination,
rename,
setElimination,
natural_numberEquality,
Error :functionIsType,
because_Cache,
universeEquality,
instantiate,
applyEquality,
functionExtensionality,
Error :universeIsType,
Error :productIsType,
sqequalRule,
voidElimination,
independent_functionElimination,
Error :lambdaFormation_alt,
hypothesisEquality,
thin,
isectElimination,
sqequalHypSubstitution,
hypothesis,
Error :isect_memberFormation_alt,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
extract_by_obid,
introduction,
cut
Latex:
\mforall{}[T:Type]. ((\mexists{}size:\mBbbN{}. T \msim{} \mBbbN{}size) {}\mRightarrow{} Fan\_d(T) {}\mRightarrow{} WKL!(T))
Date html generated:
2019_06_20-PM-02_48_11
Last ObjectModification:
2019_06_05-PM-04_27_12
Theory : fan-theorem
Home
Index