Nuprl Lemma : weak-Markov-principle

`∀a,b:ℕ ⟶ ℕ.`
`  ((∀c:ℕ ⟶ ℕ. ((¬¬(∃n:ℕ. (¬((a n) = (c n) ∈ ℤ)))) ∨ (¬¬(∃n:ℕ. (¬((b n) = (c n) ∈ ℤ))))))`
`  `` (∃n:ℕ. (¬((a n) = (b n) ∈ ℤ))))`

Proof

Definitions occuring in Statement :  nat: `ℕ` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` not: `¬A` implies: `P `` Q` or: `P ∨ Q` apply: `f a` function: `x:A ⟶ B[x]` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  rev_implies: `P `` Q` and: `P ∧ Q` iff: `P `⇐⇒` Q` uimplies: `b supposing a` squash: `↓T` exists: `∃x:A. B[x]` true: `True` so_apply: `x[s]` subtype_rel: `A ⊆r B` so_lambda: `λ2x.t[x]` guard: `{T}` uall: `∀[x:A]. B[x]` prop: `ℙ` false: `False` not: `¬A` or: `P ∨ Q` implies: `P `` Q` member: `t ∈ T` all: `∀x:A. B[x]`
Lemmas referenced :  iff_weakening_equal true_wf squash_wf exists_wf or_wf all_wf not_wf nat_wf equal_wf weak-Markov-principle-alt
Rules used in proof :  independent_isectElimination baseClosed imageMemberEquality universeEquality equalitySymmetry equalityTransitivity imageElimination productElimination natural_numberEquality intEquality lambdaEquality because_Cache inrFormation sqequalRule applyEquality functionExtensionality functionEquality isectElimination voidElimination inlFormation unionElimination independent_functionElimination hypothesisEquality thin dependent_functionElimination sqequalHypSubstitution hypothesis lambdaFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution extract_by_obid introduction cut

Latex:
\mforall{}a,b:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.
((\mforall{}c:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  ((\mneg{}\mneg{}(\mexists{}n:\mBbbN{}.  (\mneg{}((a  n)  =  (c  n)))))  \mvee{}  (\mneg{}\mneg{}(\mexists{}n:\mBbbN{}.  (\mneg{}((b  n)  =  (c  n)))))))
{}\mRightarrow{}  (\mexists{}n:\mBbbN{}.  (\mneg{}((a  n)  =  (b  n)))))

Date html generated: 2017_09_29-PM-06_06_46
Last ObjectModification: 2017_08_30-PM-00_28_08

Theory : continuity

Home Index