### Nuprl Lemma : compact-nat-inf

`∀p:ℕ∞ ⟶ 𝔹. ((∃x:ℕ∞. p x = ff) ∨ (∀x:ℕ∞. p x = tt))`

Proof

Definitions occuring in Statement :  nat-inf: `ℕ∞` bfalse: `ff` btrue: `tt` bool: `𝔹` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` or: `P ∨ Q` apply: `f a` function: `x:A ⟶ B[x]` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` uall: `∀[x:A]. B[x]` implies: `P `` Q` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` bfalse: `ff` or: `P ∨ Q` exists: `∃x:A. B[x]` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` not: `¬A` false: `False` iff: `P `⇐⇒` Q` and: `P ∧ Q` guard: `{T}` uimplies: `b supposing a` assert: `↑b` ifthenelse: `if b then t else f fi ` true: `True` rev_implies: `P `` Q`
Lemmas referenced :  nat-inf_wf ni-selector_wf bool_wf equal-wf-T-base all_wf equal_wf btrue_neq_bfalse ni-selector-property exists_wf not_wf iff_imp_equal_bool false_wf true_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut applyEquality functionExtensionality hypothesisEquality introduction extract_by_obid hypothesis sqequalHypSubstitution isectElimination thin unionElimination equalityElimination inlFormation dependent_pairFormation baseClosed sqequalRule lambdaEquality equalityTransitivity equalitySymmetry dependent_functionElimination independent_functionElimination functionEquality voidElimination addLevel impliesFunctionality productElimination inrFormation because_Cache independent_isectElimination independent_pairFormation natural_numberEquality

Latex:
\mforall{}p:\mBbbN{}\minfty{}  {}\mrightarrow{}  \mBbbB{}.  ((\mexists{}x:\mBbbN{}\minfty{}.  p  x  =  ff)  \mvee{}  (\mforall{}x:\mBbbN{}\minfty{}.  p  x  =  tt))

Date html generated: 2017_10_01-AM-08_29_30
Last ObjectModification: 2017_07_26-PM-04_24_02

Theory : basic

Home Index