Nuprl Lemma : axiom-choice-C0

`∀P:n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ ℙ. ((∀f:ℕ ⟶ 𝔹. ⇃(∃m:ℕ. (P m f))) `` ⇃(∃F:(ℕ ⟶ 𝔹) ⟶ ℕ. ∀f:ℕ ⟶ 𝔹. (P (F f) f)))`

Proof

Definitions occuring in Statement :  quotient: `x,y:A//B[x; y]` int_seg: `{i..j-}` nat: `ℕ` bool: `𝔹` prop: `ℙ` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` implies: `P `` Q` true: `True` apply: `f a` function: `x:A ⟶ B[x]` natural_number: `\$n`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` prop: `ℙ` uall: `∀[x:A]. B[x]` so_lambda: `λ2x.t[x]` subtype_rel: `A ⊆r B` so_apply: `x[s]` nat: `ℕ` uimplies: `b supposing a` le: `A ≤ B` and: `P ∧ Q` less_than': `less_than'(a;b)` false: `False` not: `¬A` exists: `∃x:A. B[x]` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` iff: `P `⇐⇒` Q` cand: `A c∧ B` guard: `{T}` pi1: `fst(t)`
Lemmas referenced :  equal_wf implies-quotient-true nat-retractible bool_subtype_base int-value-type set-value-type int_subtype_base le_wf set_subtype_base canonicalizable-function canonicalizable_wf implies-prop-truncation all-quotient-true equiv_rel_true true_wf subtype_rel_self false_wf int_seg_subtype_nat int_seg_wf subtype_rel_dep_function exists_wf quotient_wf bool_wf nat_wf all_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin functionEquality hypothesis sqequalRule lambdaEquality because_Cache applyEquality hypothesisEquality natural_numberEquality setElimination rename independent_isectElimination independent_pairFormation cumulativity universeEquality dependent_functionElimination independent_functionElimination productElimination intEquality promote_hyp dependent_pairFormation introduction equalityTransitivity equalitySymmetry

Latex:
\mforall{}P:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  \mBbbP{}
((\mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  \00D9(\mexists{}m:\mBbbN{}.  (P  m  f)))  {}\mRightarrow{}  \00D9(\mexists{}F:(\mBbbN{}  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  \mBbbN{}.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  (P  (F  f)  f)))

Date html generated: 2016_05_14-PM-09_42_27
Last ObjectModification: 2016_02_04-PM-03_51_42

Theory : continuity

Home Index