### Nuprl Lemma : stable__function_equal

`∀[A,B:Type]. ∀[f,g:A ⟶ B].  Stable{f = g ∈ (A ⟶ B)} supposing ∀x:A. Stable{(f x) = (g x) ∈ B}`

Proof

Definitions occuring in Statement :  stable: `Stable{P}` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` apply: `f a` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  stable: `Stable{P}` uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` all: `∀x:A. B[x]` not: `¬A` implies: `P `` Q` and: `P ∧ Q` prop: `ℙ` false: `False` so_lambda: `λ2x.t[x]` so_apply: `x[s]`
Lemmas referenced :  isect_wf all_wf not_wf equal_wf and_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut functionExtensionality hypothesis sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality independent_isectElimination lambdaFormation independent_functionElimination equalitySymmetry dependent_set_memberEquality independent_pairFormation lemma_by_obid isectElimination functionEquality applyEquality lambdaEquality setElimination rename productElimination setEquality voidElimination isect_memberEquality axiomEquality because_Cache equalityTransitivity universeEquality

Latex:
\mforall{}[A,B:Type].  \mforall{}[f,g:A  {}\mrightarrow{}  B].    Stable\{f  =  g\}  supposing  \mforall{}x:A.  Stable\{(f  x)  =  (g  x)\}

Date html generated: 2016_05_13-PM-03_09_31
Last ObjectModification: 2016_01_06-PM-05_27_14

Theory : core_2

Home Index