### Nuprl Lemma : not-canonicalizable-baire-to-nat

`¬⇃(canonicalizable((ℕ ⟶ ℕ) ⟶ ℕ))`

Proof

Definitions occuring in Statement :  quotient: `x,y:A//B[x; y]` canonicalizable: `canonicalizable(T)` nat: `ℕ` not: `¬A` true: `True` function: `x:A ⟶ B[x]`
Definitions unfolded in proof :  not: `¬A` all: `∀x:A. B[x]` member: `t ∈ T` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` implies: `P `` Q` uall: `∀[x:A]. B[x]` prop: `ℙ` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` uimplies: `b supposing a` subtype_rel: `A ⊆r B`
Lemmas referenced :  choice-principle_wf not_wf equiv_rel_true true_wf canonicalizable_wf quotient_wf nat_wf choice-iff-canonicalizable not-choice-baire-to-nat
Rules used in proof :  cut lemma_by_obid hypothesis addLevel sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity impliesFunctionality dependent_functionElimination thin functionEquality productElimination independent_pairFormation independent_functionElimination isectElimination because_Cache sqequalRule lambdaEquality independent_isectElimination applyEquality cumulativity hypothesisEquality universeEquality instantiate

Latex:
\mneg{}\00D9(canonicalizable((\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}))

Date html generated: 2016_05_14-PM-09_42_41
Last ObjectModification: 2016_01_13-AM-10_27_17

Theory : continuity

Home Index