### Nuprl Lemma : stable__all

`∀[T:Type]. ∀[P:T ⟶ ℙ].  ((∀x:T. Stable{P[x]}) `` Stable{∀x:T. P[x]})`

Proof

Definitions occuring in Statement :  stable: `Stable{P}` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  guard: `{T}` prop: `ℙ` all: `∀x:A. B[x]` so_apply: `x[s]` so_lambda: `λ2x.t[x]` false: `False` not: `¬A` member: `t ∈ T` uimplies: `b supposing a` stable: `Stable{P}` implies: `P `` Q` uall: `∀[x:A]. B[x]`
Lemmas referenced :  stable_wf all_wf not_wf
Rules used in proof :  independent_functionElimination independent_isectElimination universeEquality functionEquality rename hypothesis functionExtensionality applyEquality cumulativity isectElimination extract_by_obid voidElimination hypothesisEquality thin dependent_functionElimination lambdaEquality sqequalHypSubstitution sqequalRule introduction cut lambdaFormation isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].    ((\mforall{}x:T.  Stable\{P[x]\})  {}\mRightarrow{}  Stable\{\mforall{}x:T.  P[x]\})

Date html generated: 2016_10_21-AM-09_34_56
Last ObjectModification: 2016_09_26-PM-00_47_01

Theory : core_2

Home Index