Nuprl Lemma : base-member-partial

[A:Type]. ∀[a:Base]. (a ∈ partial(A)) supposing ((¬is-exception(a)) and a ∈ supposing (a)↓supposing value-type(A)


Definitions occuring in Statement :  partial: partial(T) value-type: value-type(T) has-value: (a)↓ is-exception: is-exception(t) uimplies: supposing a uall: [x:A]. B[x] not: ¬A member: t ∈ T base: Base universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] uimplies: supposing a member: t ∈ T prop: base-partial: base-partial(T) and: P ∧ Q cand: c∧ B partial: partial(T) so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] all: x:A. B[x] implies:  Q
Lemmas referenced :  has-value_wf_base equal-wf-base base_wf value-type_wf not_wf is-exception_wf base-partial_wf per-partial_wf per-partial-equiv_rel per-partial-reflex quotient-member-eq
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  sqequalRule Error :isectIsType,  Error :universeIsType,  cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis because_Cache universeEquality axiomEquality equalityTransitivity equalitySymmetry dependent_set_memberEquality independent_pairFormation productEquality isectEquality lambdaEquality setElimination rename independent_isectElimination dependent_functionElimination independent_functionElimination

    \mforall{}[a:Base].  (a  \mmember{}  partial(A))  supposing  ((\mneg{}is-exception(a))  and  a  \mmember{}  A  supposing  (a)\mdownarrow{})  supposing  valu\000Ce-type(A)

Date html generated: 2019_06_20-PM-00_33_52
Last ObjectModification: 2018_09_26-PM-01_16_40

Theory : partial_1

Home Index