### Nuprl Lemma : dfan-iff-twkl!

`∀T:Type. ((∃k:ℕ. T ~ ℕk) `` (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: `ℕ` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` iff: `P `⇐⇒` Q` implies: `P `` Q` natural_number: `\$n` universe: `Type`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` iff: `P `⇐⇒` Q` and: `P ∧ Q` uall: `∀[x:A]. B[x]` member: `t ∈ T` prop: `ℙ` rev_implies: `P `` Q` so_lambda: `λ2x.t[x]` nat: `ℕ` so_apply: `x[s]`
Lemmas referenced :  dfan-implies-twkl! dfan_wf twkl!-implies-dfan twkl!_wf exists_wf nat_wf equipollent_wf int_seg_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation independent_pairFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality independent_functionElimination hypothesis dependent_functionElimination sqequalRule lambdaEquality natural_numberEquality setElimination rename universeEquality

Latex:
\mforall{}T:Type.  ((\mexists{}k:\mBbbN{}.  T  \msim{}  \mBbbN{}k)  {}\mRightarrow{}  (Fan\_d(T)  \mLeftarrow{}{}\mRightarrow{}  WKL!(T)))

Date html generated: 2016_05_14-PM-04_12_06
Last ObjectModification: 2015_12_26-PM-07_54_10

Theory : fan-theorem

Home Index