### Nuprl Lemma : weak-Markov-principle-alt

`∀a,b:ℕ ⟶ ℕ.  ((∀c:ℕ ⟶ ℕ. ((¬(a = c ∈ (ℕ ⟶ ℕ))) ∨ (¬(b = c ∈ (ℕ ⟶ ℕ))))) `` (∃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 :  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[s]` or: `P ∨ Q` exists: `∃x:A. B[x]` nat: `ℕ` le: `A ≤ B` and: `P ∧ Q` less_than': `less_than'(a;b)` false: `False` not: `¬A` cand: `A c∧ B` uimplies: `b supposing a` sq_type: `SQType(T)` guard: `{T}` true: `True` subtype_rel: `A ⊆r B` pi1: `fst(t)` decidable: `Dec(P)` ge: `i ≥ j ` satisfiable_int_formula: `satisfiable_int_formula(fmla)` top: `Top` squash: `↓T` int_seg: `{i..j-}` lelt: `i ≤ j < k` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]`
Lemmas referenced :  all_wf nat_wf or_wf not_wf equal_wf false_wf le_wf equal-wf-base equal-wf-T-base subtype_base_sq int_subtype_base strong-continuity2-implies-weak exists_wf decidable__equal_int quotient-implies-squash int_seg_wf subtype_rel_function int_seg_subtype_nat subtype_rel_self equal-wf-base-T member_wf nat_properties full-omega-unsat intformand_wf intformnot_wf intformeq_wf itermVar_wf itermConstant_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_eq_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_wf decidable__exists_int_seg decidable__not decidable__equal_nat int_seg_properties decidable__le intformle_wf int_formula_prop_le_lemma mu-dec-property unit_wf2 it_wf mu-dec_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin functionEquality hypothesis sqequalRule lambdaEquality hypothesisEquality dependent_functionElimination unionElimination dependent_pairFormation dependent_set_memberEquality natural_numberEquality independent_pairFormation intEquality baseClosed because_Cache independent_functionElimination voidElimination productEquality setElimination rename addLevel instantiate cumulativity independent_isectElimination equalityTransitivity equalitySymmetry levelHypothesis promote_hyp productElimination applyEquality functionExtensionality applyLambdaEquality approximateComputation int_eqEquality isect_memberEquality voidEquality imageElimination imageMemberEquality

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

Date html generated: 2018_05_21-PM-01_18_17
Last ObjectModification: 2018_05_19-AM-06_37_15

Theory : continuity

Home Index