### Nuprl Lemma : per-partial-equiv_rel

`∀[T:Type]. EquivRel(base-partial(T);x,y.per-partial(T;x;y))`

Proof

Definitions occuring in Statement :  per-partial: `per-partial(T;x;y)` base-partial: `base-partial(T)` equiv_rel: `EquivRel(T;x,y.E[x; y])` uall: `∀[x:A]. B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` equiv_rel: `EquivRel(T;x,y.E[x; y])` and: `P ∧ Q` refl: `Refl(T;x,y.E[x; y])` all: `∀x:A. B[x]` cand: `A c∧ B` sym: `Sym(T;x,y.E[x; y])` implies: `P `` Q` per-partial: `per-partial(T;x;y)` uiff: `uiff(P;Q)` uimplies: `b supposing a` has-value: `(a)↓` prop: `ℙ` base-partial: `base-partial(T)` trans: `Trans(T;x,y.E[x; y])`
Lemmas referenced :  per-partial-reflex base-partial_wf has-value_wf_base per-partial_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut independent_pairFormation lambdaFormation lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis productElimination independent_isectElimination sqequalRule axiomSqleEquality setElimination rename equalitySymmetry because_Cache equalityTransitivity independent_pairEquality lambdaEquality dependent_functionElimination isect_memberEquality axiomEquality universeEquality

Latex:
\mforall{}[T:Type].  EquivRel(base-partial(T);x,y.per-partial(T;x;y))

Date html generated: 2016_05_14-AM-06_09_22
Last ObjectModification: 2015_12_26-AM-11_52_29

Theory : partial_1

Home Index