Nuprl Lemma : mu_wf

[f:ℕ ⟶ 𝔹]. mu(f) ∈ ℕ supposing ∃n:ℕ(↑(f n))


Proof




Definitions occuring in Statement :  mu: mu(f) nat: assert: b bool: 𝔹 uimplies: supposing a uall: [x:A]. B[x] exists: x:A. B[x] member: t ∈ T apply: a function: x:A ⟶ B[x]
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a mu: mu(f) subtype_rel: A ⊆B so_lambda: λ2x.t[x] so_apply: x[s] int_upper: {i...} nat: all: x:A. B[x] exists: x:A. B[x] prop:
Lemmas referenced :  mu-ge_wf subtype_rel_dep_function nat_wf bool_wf int_upper_wf subtype_rel_self assert_wf exists_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin natural_numberEquality hypothesisEquality applyEquality hypothesis lambdaEquality independent_isectElimination because_Cache lambdaFormation productElimination dependent_pairFormation axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality functionEquality

Latex:
\mforall{}[f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}].  mu(f)  \mmember{}  \mBbbN{}  supposing  \mexists{}n:\mBbbN{}.  (\muparrow{}(f  n))



Date html generated: 2016_05_14-AM-07_29_30
Last ObjectModification: 2015_12_26-PM-01_26_27

Theory : int_2


Home Index