Nuprl Lemma : cond_rel_star_monotone

[T:Type]. ∀[P:T ⟶ ℙ]. ∀[R1,R2:T ⟶ T ⟶ ℙ].  (when P, R1 => R2  R1 preserves  when P, R1^* => R2^*)


Proof




Definitions occuring in Statement :  rel_star: R^* cond_rel_implies: when P, R1 => R2 preserved_by: preserves P uall: [x:A]. B[x] prop: implies:  Q function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  rel_star: R^* cond_rel_implies: when P, 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: so_lambda: λ2x.t[x] so_apply: x[s]
Lemmas referenced :  rel_exp_wf exists_wf nat_wf preserved_by_wf all_wf cond_rel_exp_monotone
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep Error :isect_memberFormation_alt,  lambdaFormation sqequalHypSubstitution productElimination thin dependent_pairFormation hypothesisEquality cut dependent_functionElimination hypothesis independent_functionElimination applyEquality introduction extract_by_obid isectElimination lambdaEquality functionEquality Error :inhabitedIsType,  Error :functionIsType,  Error :universeIsType,  universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[R1,R2:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    (when  P,  R1  =>  R2  {}\mRightarrow{}  R1  preserves  P  {}\mRightarrow{}  when  P,  rel\_star(T;  R1)  =>  rel\_star(T;  R2))



Date html generated: 2019_06_20-PM-00_30_36
Last ObjectModification: 2018_09_26-PM-00_50_35

Theory : relations


Home Index