### Nuprl Lemma : can-apply-p-co-restrict

`∀[A,B:Type]. ∀[f:A ⟶ (B + Top)]. ∀[P:A ⟶ ℙ]. ∀[p:∀x:A. Dec(P[x])]. ∀[x:A].`
`  uiff(↑can-apply(p-co-restrict(f;p);x);(↑can-apply(f;x)) ∧ (¬P[x]))`

Proof

Definitions occuring in Statement :  p-co-restrict: `p-co-restrict(f;p)` can-apply: `can-apply(f;x)` assert: `↑b` decidable: `Dec(P)` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` top: `Top` prop: `ℙ` so_apply: `x[s]` all: `∀x:A. B[x]` not: `¬A` and: `P ∧ Q` function: `x:A ⟶ B[x]` union: `left + right` universe: `Type`
Definitions unfolded in proof :  p-co-restrict: `p-co-restrict(f;p)` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` member: `t ∈ T` uall: `∀[x:A]. B[x]` subtype_rel: `A ⊆r B` so_lambda: `λ2x.t[x]` so_apply: `x[s]` squash: `↓T` prop: `ℙ` true: `True` guard: `{T}` not: `¬A` implies: `P `` Q` false: `False` all: `∀x:A. B[x]` top: `Top` rev_uimplies: `rev_uimplies(P;Q)` iff: `P `⇐⇒` Q` rev_implies: `P `` Q`
Lemmas referenced :  can-apply-compose-iff iff_weakening_uiff decidable_wf all_wf p-co-restrict_wf uiff_wf p-compose_wf not_wf and_wf subtype_rel_union subtype_rel_dep_function assert_wf assert_witness can-apply-p-co-filter do-apply-p-co-filter top_wf true_wf squash_wf p-co-filter_wf do-apply_wf can-apply_wf assert_functionality_wrt_uiff
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity independent_pairFormation isect_memberFormation introduction cut sqequalHypSubstitution productElimination thin lemma_by_obid isectElimination hypothesisEquality applyEquality because_Cache hypothesis sqequalRule lambdaEquality independent_isectElimination imageElimination equalityTransitivity equalitySymmetry functionEquality unionEquality natural_numberEquality imageMemberEquality baseClosed lambdaFormation independent_functionElimination voidElimination independent_pairEquality dependent_functionElimination productEquality cumulativity isect_memberEquality voidEquality universeEquality addLevel

Latex:
\mforall{}[A,B:Type].  \mforall{}[f:A  {}\mrightarrow{}  (B  +  Top)].  \mforall{}[P:A  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[p:\mforall{}x:A.  Dec(P[x])].  \mforall{}[x:A].
uiff(\muparrow{}can-apply(p-co-restrict(f;p);x);(\muparrow{}can-apply(f;x))  \mwedge{}  (\mneg{}P[x]))

Date html generated: 2016_05_15-PM-03_31_29
Last ObjectModification: 2016_01_16-AM-10_49_04

Theory : general

Home Index