### Nuprl Lemma : simple-decidable-finite-cantor-ext

`∀[T:Type]. ∀[R:T ⟶ ℙ].  ((∀x:T. Dec(R[x])) `` (∀n:ℕ. ∀F:(ℕn ⟶ 𝔹) ⟶ T.  Dec(∃f:ℕn ⟶ 𝔹. R[F f])))`

Proof

Definitions occuring in Statement :  int_seg: `{i..j-}` nat: `ℕ` bool: `𝔹` decidable: `Dec(P)` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` implies: `P `` Q` apply: `f a` function: `x:A ⟶ B[x]` natural_number: `\$n` universe: `Type`
Definitions unfolded in proof :  member: `t ∈ T` it: `⋅` ifthenelse: `if b then t else f fi ` simple-finite-cantor-decider: `FiniteCantorDecide(dcdr;n;F)` simple-decidable-finite-cantor sq_stable_from_decidable sq_stable__from_stable stable__from_decidable any: `any x`
Lemmas referenced :  simple-decidable-finite-cantor sq_stable_from_decidable sq_stable__from_stable stable__from_decidable
Rules used in proof :  introduction sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut instantiate extract_by_obid hypothesis sqequalRule thin sqequalHypSubstitution equalityTransitivity equalitySymmetry

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  \mBbbP{}].    ((\mforall{}x:T.  Dec(R[x]))  {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  \mforall{}F:(\mBbbN{}n  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  T.    Dec(\mexists{}f:\mBbbN{}n  {}\mrightarrow{}  \mBbbB{}.  R[F  f])))

Date html generated: 2018_05_21-PM-01_17_25
Last ObjectModification: 2018_05_19-AM-06_32_32

Theory : continuity

Home Index