Nuprl Lemma : notAC20

`∀T:Type`
`  (⇃T`
`  `` (¬(∀P:((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ T ⟶ ℙ`
`          ((∀n:(ℕ ⟶ ℕ) ⟶ ℕ. ⇃∃m:T. (P n m)) `` ⇃∃f:((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ T. ∀n:(ℕ ⟶ ℕ) ⟶ ℕ. (P n (f n))))))`

Proof

Definitions occuring in Statement :  qsquash: `⇃T` nat: `ℕ` prop: `ℙ` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` not: `¬A` implies: `P `` Q` apply: `f a` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` not: `¬A` false: `False` member: `t ∈ T` prop: `ℙ` uall: `∀[x:A]. B[x]` subtype_rel: `A ⊆r B` so_lambda: `λ2x.t[x]` so_apply: `x[s]` exists: `∃x:A. B[x]` choice-principle: `ChoicePrinciple(T)` iff: `P `⇐⇒` Q` and: `P ∧ Q` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` uimplies: `b supposing a` rev_implies: `P `` Q` qsquash: `⇃T` true: `True` cand: `A c∧ B` quotient: `x,y:A//B[x; y]` squash: `↓T` guard: `{T}`
Lemmas referenced :  squash_wf member_wf equal-wf-base quotient-member-eq prop-truncation-quot equiv_rel_true true_wf quotient_wf not-choice-baire-to-nat exists_wf qsquash_wf nat_wf all_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut thin because_Cache hypothesis sqequalHypSubstitution independent_functionElimination voidElimination instantiate lemma_by_obid isectElimination functionEquality applyEquality lambdaEquality cumulativity hypothesisEquality universeEquality sqequalRule functionExtensionality independent_pairFormation independent_isectElimination dependent_functionElimination rename introduction promote_hyp equalityTransitivity equalitySymmetry natural_numberEquality pointwiseFunctionality pertypeElimination productElimination productEquality imageElimination imageMemberEquality baseClosed dependent_pairFormation

Latex:
\mforall{}T:Type
(\00D9T
{}\mRightarrow{}  (\mneg{}(\mforall{}P:((\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
((\mforall{}n:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.  \00D9\mexists{}m:T.  (P  n  m))
{}\mRightarrow{}  \00D9\mexists{}f:((\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  T.  \mforall{}n:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.  (P  n  (f  n))))))

Date html generated: 2016_05_14-PM-09_42_52
Last ObjectModification: 2016_04_05-PM-05_12_24

Theory : continuity

Home Index