Nuprl Lemma : rel_plus_functionality_wrt_rel_implies

[T:Type]. ∀[R1,R2:T ⟶ T ⟶ ℙ].  (R1 => R2  R1+ => R2+)


Proof




Definitions occuring in Statement :  rel_plus: R+ rel_implies: R1 => R2 uall: [x:A]. B[x] prop: implies:  Q function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  rel_plus: R+ rel_implies: R1 => R2 infix_ap: y uall: [x:A]. B[x] implies:  Q all: x:A. B[x] exists: x:A. B[x] member: t ∈ T prop: subtype_rel: A ⊆B so_lambda: λ2x.t[x] so_apply: x[s]
Lemmas referenced :  rel_exp_wf exists_wf nat_plus_wf nat_plus_subtype_nat all_wf rel_exp_monotone
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation lambdaFormation sqequalHypSubstitution productElimination thin dependent_pairFormation hypothesisEquality cut dependent_functionElimination hypothesis independent_functionElimination applyEquality lemma_by_obid isectElimination because_Cache lambdaEquality functionEquality cumulativity universeEquality

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



Date html generated: 2016_05_14-PM-03_54_01
Last ObjectModification: 2015_12_26-PM-06_56_15

Theory : relations2


Home Index