### Nuprl Lemma : mu-bound-property

`∀[b:ℕ]. ∀[f:ℕb ⟶ 𝔹].  {(↑(f mu(f))) ∧ (∀[i:ℕb]. ¬↑(f i) supposing i < mu(f))} supposing ∃n:ℕb. (↑(f n))`

Proof

Definitions occuring in Statement :  mu: `mu(f)` int_seg: `{i..j-}` nat: `ℕ` assert: `↑b` bool: `𝔹` less_than: `a < b` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` guard: `{T}` exists: `∃x:A. B[x]` not: `¬A` and: `P ∧ Q` apply: `f a` function: `x:A ⟶ B[x]` natural_number: `\$n`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` uimplies: `b supposing a` member: `t ∈ T` guard: `{T}` nat: `ℕ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` exists: `∃x:A. B[x]` prop: `ℙ` int_seg: `{i..j-}` subtype_rel: `A ⊆r B` implies: `P `` Q` sq_stable: `SqStable(P)` not: `¬A` false: `False` squash: `↓T` all: `∀x:A. B[x]` mu: `mu(f)` and: `P ∧ Q` cand: `A c∧ B` lelt: `i ≤ j < k` le: `A ≤ B` less_than: `a < b`
Lemmas referenced :  lelt_wf mu-ge-bound-property assert_witness sq_stable__not sq_stable__uall sq_stable__and squash_wf not_wf less_than_wf isect_wf uall_wf nat_wf bool_wf assert_wf int_seg_wf exists_wf mu-bound
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality independent_isectElimination hypothesis natural_numberEquality setElimination rename sqequalRule lambdaEquality applyEquality functionEquality isect_memberEquality equalityTransitivity equalitySymmetry because_Cache independent_functionElimination lambdaFormation introduction dependent_functionElimination voidElimination imageMemberEquality baseClosed imageElimination productElimination independent_pairFormation dependent_set_memberEquality

Latex:
\mforall{}[b:\mBbbN{}].  \mforall{}[f:\mBbbN{}b  {}\mrightarrow{}  \mBbbB{}].
\{(\muparrow{}(f  mu(f)))  \mwedge{}  (\mforall{}[i:\mBbbN{}b].  \mneg{}\muparrow{}(f  i)  supposing  i  <  mu(f))\}  supposing  \mexists{}n:\mBbbN{}b.  (\muparrow{}(f  n))

Date html generated: 2016_05_14-AM-07_29_57
Last ObjectModification: 2016_01_14-PM-09_58_51

Theory : int_2

Home Index