### Nuprl Lemma : rel_plus_functionality_wrt_breqv

`∀[T:Type]. ∀[R1,R2:T ⟶ T ⟶ ℙ].  ((R1 <≡>{T} R2) `` (R1+ <≡>{T} R2+))`

Proof

Definitions occuring in Statement :  binrel_eqv: `E <≡>{T} E'` rel_plus: `R+` uall: `∀[x:A]. B[x]` prop: `ℙ` implies: `P `` Q` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` implies: `P `` Q` member: `t ∈ T` prop: `ℙ` guard: `{T}`
Lemmas referenced :  binrel_le_antisymmetry rel_plus_wf rel_plus_functionality_wrt_brle binrel_le_weakening binrel_eqv_inversion binrel_eqv_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality sqequalRule hypothesis independent_functionElimination because_Cache functionEquality cumulativity universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[R1,R2:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    ((R1  <\mequiv{}>\{T\}  R2)  {}\mRightarrow{}  (R1\msupplus{}  <\mequiv{}>\{T\}  R2\msupplus{}))

Date html generated: 2016_05_14-PM-03_55_05
Last ObjectModification: 2015_12_26-PM-06_55_45

Theory : relations2

Home Index