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

`sOvert(ℕ) `` (∀g:ℕ ⟶ 𝔹. ((¬(∀n:ℕ. g n = ff)) `` (∃n:ℕ. g 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: `P `` Q` apply: `f a` function: `x:A ⟶ B[x]` equal: `s = t ∈ T`
Definitions unfolded in proof :  implies: `P `` 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 ⊆r B` pi1: `fst(t)` iff: `P `⇐⇒` Q` and: `P ∧ Q` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` uimplies: `b supposing a` bfalse: `ff` or: `P ∨ Q` sq_type: `SQType(T)` guard: `{T}` bnot: `¬bb` ifthenelse: `if b then t else f fi ` assert: `↑b` false: `False` not: `¬A` rev_implies: `P `` 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