### Nuprl Lemma : rel_exp_functionality_wrt_breqv

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

Proof

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

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

Date html generated: 2016_05_14-PM-03_55_10
Last ObjectModification: 2015_12_26-PM-06_55_34

Theory : relations2

Home Index