### Nuprl Lemma : decidable__equal_compact_domain

`∀[T,S:Type].  ((∀a,b:S.  Dec(a = b ∈ S)) `` compact-type(T) `` (∀f,g:T ⟶ S.  Dec(f = g ∈ (T ⟶ S))))`

Proof

Definitions occuring in Statement :  compact-type: `compact-type(T)` decidable: `Dec(P)` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` implies: `P `` Q` all: `∀x:A. B[x]` member: `t ∈ T` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` compact-type: `compact-type(T)` deq: `EqDecider(T)` or: `P ∨ Q` decidable: `Dec(P)` not: `¬A` false: `False` exists: `∃x:A. B[x]` uiff: `uiff(P;Q)` uimplies: `b supposing a` eqof: `eqof(d)`
Lemmas referenced :  deq-exists compact-type_wf all_wf decidable_wf equal_wf equal-wf-T-base bool_wf eqff_to_assert assert_wf bnot_wf eqof_wf not_wf iff_transitivity iff_weakening_uiff assert_of_bnot safe-assert-deq eqtt_to_assert
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality productElimination independent_functionElimination hypothesis rename functionEquality cumulativity sqequalRule lambdaEquality universeEquality dependent_functionElimination applyEquality setElimination functionExtensionality unionElimination inrFormation because_Cache equalitySymmetry hyp_replacement applyLambdaEquality baseClosed equalityTransitivity independent_isectElimination voidElimination independent_pairFormation impliesFunctionality promote_hyp inlFormation

Latex:
\mforall{}[T,S:Type].    ((\mforall{}a,b:S.    Dec(a  =  b))  {}\mRightarrow{}  compact-type(T)  {}\mRightarrow{}  (\mforall{}f,g:T  {}\mrightarrow{}  S.    Dec(f  =  g)))

Date html generated: 2017_10_01-AM-08_29_08
Last ObjectModification: 2017_07_26-PM-04_23_49

Theory : basic

Home Index