Nuprl Lemma : dec_alt_char_a

[T:Type]. ∀[A:T ⟶ ℙ].  (∀x:T. Dec(A x) ⇐⇒ (∀x:T. SqStable(A x)) ∧ detach_fun(T;A))


Proof




Definitions occuring in Statement :  detach_fun: detach_fun(T;A) sq_stable: SqStable(P) decidable: Dec(P) uall: [x:A]. B[x] prop: all: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q apply: a function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] iff: ⇐⇒ Q and: P ∧ Q implies:  Q all: x:A. B[x] member: t ∈ T prop: so_lambda: λ2x.t[x] so_apply: x[s] rev_implies:  Q guard: {T}
Lemmas referenced :  all_wf decidable_wf and_wf sq_stable_wf detach_fun_wf sq_stable_from_decidable exists_det_fun exists_det_fun_a
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation independent_pairFormation lambdaFormation hypothesisEquality cut lemma_by_obid sqequalHypSubstitution isectElimination thin sqequalRule lambdaEquality applyEquality hypothesis functionEquality cumulativity universeEquality independent_functionElimination dependent_functionElimination because_Cache productElimination

Latex:
\mforall{}[T:Type].  \mforall{}[A:T  {}\mrightarrow{}  \mBbbP{}].    (\mforall{}x:T.  Dec(A  x)  \mLeftarrow{}{}\mRightarrow{}  (\mforall{}x:T.  SqStable(A  x))  \mwedge{}  detach\_fun(T;A))



Date html generated: 2016_05_15-PM-00_00_32
Last ObjectModification: 2015_12_26-PM-11_26_45

Theory : gen_algebra_1


Home Index