### Nuprl Lemma : change-from1_wf

`∀[a:ℕ ⟶ ℕ]. (change-from1(a) ∈ ℕ ⟶ 𝔹)`

Proof

Definitions occuring in Statement :  change-from1: `change-from1(a)` nat: `ℕ` bool: `𝔹` uall: `∀[x:A]. B[x]` member: `t ∈ T` function: `x:A ⟶ B[x]`
Definitions unfolded in proof :  subtype_rel: `A ⊆r B` prop: `ℙ` less_than': `less_than'(a;b)` and: `P ∧ Q` le: `A ≤ B` not: `¬A` implies: `P `` Q` false: `False` nat: `ℕ` change-from1: `change-from1(a)` member: `t ∈ T` uall: `∀[x:A]. B[x]`
Lemmas referenced :  btrue_wf le_wf false_wf nat_wf bfalse_wf
Rules used in proof :  functionEquality equalitySymmetry equalityTransitivity axiomEquality isectElimination lambdaFormation independent_pairFormation dependent_set_memberEquality hypothesisEquality functionExtensionality applyEquality extract_by_obid natural_numberEquality hypothesis because_Cache rename thin setElimination sqequalHypSubstitution int_eqEquality lambdaEquality sqequalRule cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[a:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}].  (change-from1(a)  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{})

Date html generated: 2017_04_21-AM-11_23_23
Last ObjectModification: 2017_04_20-PM-04_55_51

Theory : continuity

Home Index