Nuprl Lemma : fpf-cap_functionality_wrt_sub

[A:Type]. ∀[d1,d2,d3,d4:EqDecider(A)]. ∀[B:A ⟶ Type]. ∀[f,g:a:A fp-> B[a]]. ∀[x:A]. ∀[z:B[x]].
  (f(x)?z g(x)?z ∈ B[x]) supposing ((↑x ∈ dom(f)) and f ⊆ g)


Definitions occuring in Statement :  fpf-sub: f ⊆ g fpf-cap: f(x)?z fpf-dom: x ∈ dom(f) fpf: a:A fp-> B[a] deq: EqDecider(T) assert: b uimplies: supposing a uall: [x:A]. B[x] so_apply: x[s] function: x:A ⟶ B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  bfalse: ff ifthenelse: if then else fi  and: P ∧ Q uiff: uiff(P;Q) btrue: tt it: unit: Unit bool: 𝔹 implies:  Q top: Top all: x:A. B[x] so_apply: x[s] so_lambda: λ2x.t[x] subtype_rel: A ⊆B prop: fpf-cap: f(x)?z uimplies: supposing a member: t ∈ T uall: [x:A]. B[x] pi2: snd(t) fpf-ap: f(x) cand: c∧ B guard: {T} fpf-sub: f ⊆ g false: False not: ¬A
Lemmas referenced :  equal_wf assert_of_bnot eqff_to_assert uiff_transitivity eqtt_to_assert not_wf bnot_wf equal-wf-T-base bool_wf deq_wf fpf_wf fpf-sub_wf top_wf subtype-fpf2 fpf-dom_wf assert_wf fpf-dom_functionality2
Rules used in proof :  dependent_functionElimination independent_functionElimination productElimination equalityElimination unionElimination baseClosed equalitySymmetry equalityTransitivity axiomEquality because_Cache voidEquality voidElimination isect_memberEquality lambdaFormation independent_isectElimination functionExtensionality lambdaEquality sqequalRule applyEquality hypothesisEquality cumulativity thin isectElimination sqequalHypSubstitution extract_by_obid hypothesis cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution universeIsType Error :memTop,  lambdaFormation_alt inhabitedIsType lambdaEquality_alt

\mforall{}[A:Type].  \mforall{}[d1,d2,d3,d4:EqDecider(A)].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[f,g:a:A  fp->  B[a]].  \mforall{}[x:A].  \mforall{}[z:B[x]].
    (f(x)?z  =  g(x)?z)  supposing  ((\muparrow{}x  \mmember{}  dom(f))  and  f  \msubseteq{}  g)

Date html generated: 2020_05_20-AM-09_02_24
Last ObjectModification: 2020_01_25-AM-11_42_15

Theory : finite!partial!functions

Home Index