Nuprl Lemma : nat-strong-overt-implies-Markov

sOvert(ℕ (∀g:ℕ ⟶ 𝔹((¬(∀n:ℕff))  (∃n:ℕtt)))


Proof




Definitions occuring in Statement :  strong-overt: sOvert(X) nat: bfalse: ff btrue: tt bool: 𝔹 all: x:A. B[x] exists: x:A. B[x] not: ¬A implies:  Q apply: a function: x:A ⟶ B[x] equal: t ∈ T
Definitions unfolded in proof :  implies:  Q all: x:A. B[x] strong-overt: sOvert(X) member: t ∈ T exists: x:A. B[x] in-open: x ∈ A Open: Open(X) prop: uall: [x:A]. B[x] so_lambda: λ2x.t[x] so_apply: x[s] top: Top subtype_rel: A ⊆B pi1: fst(t) iff: ⇐⇒ Q and: P ∧ Q bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) uimplies: supposing a bfalse: ff or: P ∨ Q sq_type: SQType(T) guard: {T} bnot: ¬bb ifthenelse: if then else fi  assert: b false: False not: ¬A rev_implies:  Q true: True
Lemmas referenced :  unit_wf2 not_wf all_wf nat_wf equal-wf-T-base bool_wf strong-overt_wf ifthenelse_wf pi1_wf_top Sierpinski_wf Sierpinski-top_wf subtype-Sierpinski Sierpinski-bottom_wf it_wf Sierpinski-unequal eqtt_to_assert btrue_wf eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot exists_wf btrue_neq_bfalse not-Sierpinski-bottom rev_implies_wf bfalse_wf iff_imp_equal_bool assert_wf true_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation sqequalHypSubstitution dependent_functionElimination thin cut introduction extract_by_obid hypothesis productElimination sqequalRule isectElimination lambdaEquality applyEquality functionExtensionality hypothesisEquality baseClosed functionEquality independent_pairEquality isect_memberEquality voidElimination voidEquality productEquality independent_pairFormation dependent_pairFormation unionElimination equalityElimination equalityTransitivity equalitySymmetry independent_isectElimination promote_hyp instantiate cumulativity independent_functionElimination because_Cache hyp_replacement applyLambdaEquality natural_numberEquality

Latex:
sOvert(\mBbbN{})  {}\mRightarrow{}  (\mforall{}g:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  ((\mneg{}(\mforall{}n:\mBbbN{}.  g  n  =  ff))  {}\mRightarrow{}  (\mexists{}n:\mBbbN{}.  g  n  =  tt)))



Date html generated: 2019_10_31-AM-07_19_28
Last ObjectModification: 2017_07_28-AM-09_12_29

Theory : synthetic!topology


Home Index