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

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

Proof

Definitions occuring in Statement :  int_seg: `{i..j-}` nat: `ℕ` bool: `𝔹` decidable: `Dec(P)` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s1;s2]` 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 ` finite-cantor-decider: `finite-cantor-decider(dcdr;n;F)` decidable-finite-cantor sq_stable_from_decidable sq_stable__from_stable stable__from_decidable any: `any x`
Lemmas referenced :  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{}  T  {}\mrightarrow{}  \mBbbP{}].
((\mforall{}x,y:T.    Dec(R[x;y]))  {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  \mforall{}F:(\mBbbN{}n  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  T.    Dec(\mexists{}f,g:\mBbbN{}n  {}\mrightarrow{}  \mBbbB{}.  R[F  f;F  g])))

Date html generated: 2018_05_21-PM-01_17_19
Last ObjectModification: 2018_05_19-AM-06_32_33

Theory : continuity

Home Index