Nuprl Lemma : assert-finite-fun-deq

[T:Type]. ∀[k:ℕ]. ∀[eq:EqDecider(T)]. ∀[f,g:ℕk ⟶ T].  uiff(↑(finite-fun-deq(k;eq) g);f g ∈ (ℕk ⟶ T))


Proof




Definitions occuring in Statement :  finite-fun-deq: finite-fun-deq(k;eq) deq: EqDecider(T) int_seg: {i..j-} nat: assert: b uiff: uiff(P;Q) uall: [x:A]. B[x] apply: a function: x:A ⟶ B[x] natural_number: $n universe: Type equal: t ∈ T
Definitions unfolded in proof :  uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a member: t ∈ T uall: [x:A]. B[x] subtype_rel: A ⊆B deq: EqDecider(T) nat: implies:  Q iff: ⇐⇒ Q rev_implies:  Q
Lemmas referenced :  iff_weakening_uiff assert_wf finite-fun-deq_wf equal_wf int_seg_wf assert-deq istype-assert assert_witness deq_wf istype-nat istype-universe
Rules used in proof :  cut sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity independent_pairFormation isect_memberFormation_alt hypothesis equalityIstype inhabitedIsType hypothesisEquality because_Cache sqequalHypSubstitution productElimination thin independent_isectElimination introduction extract_by_obid isectElimination applyEquality lambdaEquality_alt setElimination rename equalityTransitivity equalitySymmetry sqequalRule functionEquality natural_numberEquality independent_functionElimination promote_hyp functionIsType universeIsType instantiate universeEquality independent_pairEquality isect_memberEquality_alt axiomEquality isectIsTypeImplies

Latex:
\mforall{}[T:Type].  \mforall{}[k:\mBbbN{}].  \mforall{}[eq:EqDecider(T)].  \mforall{}[f,g:\mBbbN{}k  {}\mrightarrow{}  T].    uiff(\muparrow{}(finite-fun-deq(k;eq)  f  g);f  =  g)



Date html generated: 2020_05_19-PM-09_36_36
Last ObjectModification: 2019_10_18-PM-00_01_10

Theory : equality!deciders


Home Index