### Nuprl Lemma : general-fan-theorem-troelstra-sq

`∀X:n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ ℙ. ((∀f:ℕ ⟶ 𝔹. ⇃(∃n:ℕ. X[n;f])) `` ⇃(∃k:ℕ. ∀f:ℕ ⟶ 𝔹. ∃n:ℕk. X[n;f]))`

Proof

Definitions occuring in Statement :  quotient: `x,y:A//B[x; y]` int_seg: `{i..j-}` nat: `ℕ` bool: `𝔹` prop: `ℙ` so_apply: `x[s1;s2]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` implies: `P `` Q` true: `True` 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]` so_apply: `x[s1;s2]` 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]` int_seg: `{i..j-}` guard: `{T}`
Lemmas referenced :  general-fan-theorem-troelstra implies-quotient-true prop-truncation-quot axiom-choice-C0 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 dependent_pairFormation

Latex:
\mforall{}X:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  \mBbbP{}.  ((\mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  \00D9(\mexists{}n:\mBbbN{}.  X[n;f]))  {}\mRightarrow{}  \00D9(\mexists{}k:\mBbbN{}.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  \mexists{}n:\mBbbN{}k.  X[n;f]))

Date html generated: 2016_05_14-PM-09_54_06
Last ObjectModification: 2016_02_04-PM-03_55_09

Theory : continuity

Home Index