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