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 ⊆B prop: less_than': less_than'(a;b) and: P ∧ Q le: A ≤ B not: ¬A implies:  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