### Nuprl Lemma : fpf-dom_functionality

`∀[A:Type]. ∀[B:A ⟶ Type]. ∀[eq1,eq2:EqDecider(A)]. ∀[f:a:A fp-> B[a]]. ∀[x:A].  x ∈ dom(f) = x ∈ dom(f)`

Proof

Definitions occuring in Statement :  fpf-dom: `x ∈ dom(f)` fpf: `a:A fp-> B[a]` deq: `EqDecider(T)` bool: `𝔹` uall: `∀[x:A]. B[x]` so_apply: `x[s]` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` fpf-dom: `x ∈ dom(f)` fpf: `a:A fp-> B[a]` pi1: `fst(t)` all: `∀x:A. B[x]` implies: `P `` Q` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` iff: `P `⇐⇒` Q` prop: `ℙ` rev_implies: `P `` Q` true: `True` assert: `↑b` ifthenelse: `if b then t else f fi ` bfalse: `ff` exists: `∃x:A. B[x]` or: `P ∨ Q` sq_type: `SQType(T)` guard: `{T}` bnot: `¬bb` false: `False` not: `¬A` so_lambda: `λ2x.t[x]` so_apply: `x[s]`
Lemmas referenced :  deq-member_wf bool_wf eqtt_to_assert assert-deq-member iff_imp_equal_bool btrue_wf true_wf l_member_wf assert_wf iff_wf eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot bfalse_wf false_wf fpf_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution productElimination thin sqequalRule extract_by_obid isectElimination cumulativity hypothesisEquality hypothesis lambdaFormation unionElimination equalityElimination equalityTransitivity equalitySymmetry independent_isectElimination dependent_functionElimination independent_functionElimination independent_pairFormation natural_numberEquality addLevel impliesFunctionality because_Cache dependent_pairFormation promote_hyp instantiate voidElimination isect_memberEquality axiomEquality lambdaEquality applyEquality functionExtensionality functionEquality universeEquality

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

Date html generated: 2018_05_21-PM-09_17_30
Last ObjectModification: 2018_02_09-AM-10_16_32

Theory : finite!partial!functions

Home Index