### Nuprl Lemma : fpf-dom_functionality2

[A:Type]. ∀[eq1,eq2:EqDecider(A)]. ∀[f:a:A fp-> Top]. ∀[x:A].  {↑x ∈ dom(f) supposing ↑x ∈ dom(f)}

Proof

Definitions occuring in Statement :  fpf-dom: x ∈ dom(f) fpf: a:A fp-> B[a] deq: EqDecider(T) assert: b uimplies: supposing a uall: [x:A]. B[x] top: Top guard: {T} universe: Type
Definitions unfolded in proof :  guard: {T} uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a so_lambda: λ2x.t[x] so_apply: x[s] prop: implies:  Q
Lemmas referenced :  fpf-dom_functionality top_wf assert_wf assert_witness fpf-dom_wf fpf_wf deq_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin because_Cache lambdaEquality hypothesis cumulativity hypothesisEquality hyp_replacement equalitySymmetry applyLambdaEquality independent_functionElimination isect_memberEquality equalityTransitivity universeEquality

Latex:
\mforall{}[A:Type].  \mforall{}[eq1,eq2:EqDecider(A)].  \mforall{}[f:a:A  fp->  Top].  \mforall{}[x:A].    \{\muparrow{}x  \mmember{}  dom(f)  supposing  \muparrow{}x  \mmember{}  dom(f)\}

Date html generated: 2018_05_21-PM-09_17_31
Last ObjectModification: 2018_02_09-AM-10_16_33

Theory : finite!partial!functions

Home Index