### Nuprl Lemma : finite-cantor-decider_wf

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

Proof

Definitions occuring in Statement :  finite-cantor-decider: `finite-cantor-decider(dcdr;n;F)` 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]` member: `t ∈ T` apply: `f a` function: `x:A ⟶ B[x]` natural_number: `\$n` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` all: `∀x:A. B[x]` nat: `ℕ` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s1;s2]` so_apply: `x[s]` decidable-finite-cantor-ext implies: `P `` Q` subtype_rel: `A ⊆r B` exists: `∃x:A. B[x]`
Lemmas referenced :  int_seg_wf bool_wf nat_wf all_wf decidable_wf decidable-finite-cantor-ext uall_wf exists_wf isect_wf equal_wf subtype_rel_self
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation sqequalHypSubstitution hypothesis functionEquality extract_by_obid isectElimination thin natural_numberEquality setElimination rename hypothesisEquality sqequalRule lambdaEquality applyEquality dependent_functionElimination axiomEquality equalityTransitivity equalitySymmetry because_Cache cumulativity universeEquality isect_memberEquality instantiate independent_functionElimination isectEquality

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
\mforall{}dcdr:\mforall{}x,y:T.    Dec(R[x;y]).  \mforall{}n:\mBbbN{}.  \mforall{}F:(\mBbbN{}n  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  T.
(finite-cantor-decider(dcdr;n;F)  \mmember{}  Dec(\mexists{}f,g:\mBbbN{}n  {}\mrightarrow{}  \mBbbB{}.  R[F  f;F  g]))

Date html generated: 2019_06_20-PM-02_49_52
Last ObjectModification: 2018_09_26-AM-09_54_21

Theory : continuity

Home Index