### Nuprl Lemma : intuitionistic-pigeonhole

`∀A,B:ℕ ⟶ ℙ.`
`  ((∀s:StrictInc. ⇃(∃n:ℕ. A[s n])) `` (∀s:StrictInc. ⇃(∃n:ℕ. B[s n])) `` (∀s:StrictInc. ⇃(∃n:ℕ. (A[s n] ∧ B[s n]))))`

Proof

Definitions occuring in Statement :  strict-inc: `StrictInc` quotient: `x,y:A//B[x; y]` nat: `ℕ` prop: `ℙ` so_apply: `x[s]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` implies: `P `` Q` and: `P ∧ Q` true: `True` apply: `f a` function: `x:A ⟶ B[x]`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` so_lambda: `λ2x.t[x]` member: `t ∈ T` so_apply: `x[s]` strict-inc: `StrictInc` prop: `ℙ` uall: `∀[x:A]. B[x]` exists: `∃x:A. B[x]` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` uimplies: `b supposing a` compose: `f o g` nat: `ℕ` subtype_rel: `A ⊆r B` guard: `{T}` cand: `A c∧ B` and: `P ∧ Q`
Lemmas referenced :  two-implies-quotient-true and_wf implies-quotient-true canonicalizable-nat-to-nat less_than_wf int_seg_wf canonicalizable-set canonicalizable_wf trivial-quotient-true axiom-choice-quot compose-strict-inc equiv_rel_true true_wf exists_wf quotient_wf all_wf strict-inc_wf nat_wf unary-almost-full-has-strict-inc
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut lemma_by_obid sqequalHypSubstitution dependent_functionElimination thin sqequalRule lambdaEquality applyEquality hypothesisEquality setElimination rename hypothesis independent_functionElimination because_Cache isectElimination independent_isectElimination functionEquality cumulativity universeEquality natural_numberEquality productElimination dependent_pairFormation independent_pairFormation

Latex:
\mforall{}A,B:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}.
((\mforall{}s:StrictInc.  \00D9(\mexists{}n:\mBbbN{}.  A[s  n]))
{}\mRightarrow{}  (\mforall{}s:StrictInc.  \00D9(\mexists{}n:\mBbbN{}.  B[s  n]))
{}\mRightarrow{}  (\mforall{}s:StrictInc.  \00D9(\mexists{}n:\mBbbN{}.  (A[s  n]  \mwedge{}  B[s  n]))))

Date html generated: 2016_05_14-PM-09_48_45
Last ObjectModification: 2016_01_06-PM-09_29_05

Theory : continuity

Home Index