Nuprl Lemma : fan-wkl!
∀[T:Type]. ((∃size:ℕ. T ~ ℕsize) ⇒ Fan(T) ⇒ WKL!(T))
Proof
Definitions occuring in Statement :
alt-wkl!: WKL!(T),
altfan: Fan(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 :
exists: ∃x:A. B[x],
and: P ∧ Q,
nat: ℕ,
prop: ℙ,
uimplies: b supposing a,
false: False,
not: ¬A,
all: ∀x:A. B[x],
implies: P ⇒ Q,
member: t ∈ T,
uall: ∀[x:A]. B[x]
Lemmas referenced :
istype-universe,
equipollent_wf,
altfan_wf,
altunbounded_wf,
alttree_wf,
bool_wf,
int_seg_wf,
istype-nat,
altneg_wf,
altbar_wf,
istype-void,
complement-unbounded-tree,
fan-bar-sep,
alt-bar-sep-wkl!
Rules used in proof :
universeEquality,
instantiate,
Error :productIsType,
natural_numberEquality,
Error :setIsType,
rename,
setElimination,
Error :universeIsType,
dependent_functionElimination,
Error :inhabitedIsType,
Error :functionIsType,
sqequalRule,
voidElimination,
independent_isectElimination,
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(T) {}\mRightarrow{} WKL!(T))
Date html generated:
2019_06_20-PM-02_46_57
Last ObjectModification:
2019_06_07-PM-00_00_05
Theory : fan-theorem
Home
Index