Nuprl Lemma : rel_exp_monotone

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


Proof




Definitions occuring in Statement :  rel_implies: R1 => R2 rel_exp: R^n nat: uall: [x:A]. B[x] prop: all: x:A. B[x] implies:  Q function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q member: t ∈ T prop: uall: [x:A]. B[x] so_lambda: λ2x.t[x] subtype_rel: A ⊆B nat: decidable: Dec(P) or: P ∨ Q iff: ⇐⇒ Q and: P ∧ Q not: ¬A rev_implies:  Q false: False uiff: uiff(P;Q) uimplies: supposing a subtract: m top: Top le: A ≤ B less_than': less_than'(a;b) true: True so_apply: x[s] rel_implies: R1 => R2 rel_exp: R^n eq_int: (i =z j) ifthenelse: if then else fi  btrue: tt infix_ap: y guard: {T} exists: x:A. B[x] cand: c∧ B bool: 𝔹 unit: Unit it: bfalse: ff
Lemmas referenced :  uall_wf rel_implies_wf rel_exp_wf subtract_wf decidable__le false_wf not-le-2 less-iff-le condition-implies-le minus-one-mul zero-add minus-one-mul-top minus-add minus-minus add-associates add-swap add-commutes add_functionality_wrt_le add-zero le-add-cancel le_wf set_wf less_than_wf primrec-wf2 nat_wf equal_wf all_wf eq_int_wf bool_wf equal-wf-base int_subtype_base assert_wf less_than_transitivity1 le_weakening less_than_irreflexivity bnot_wf not_wf infix_ap_wf subtype_rel_self exists_wf uiff_transitivity eqtt_to_assert assert_of_eq_int eqff_to_assert assert_of_bnot not_functionality_wrt_uiff
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut thin rename setElimination instantiate introduction extract_by_obid sqequalHypSubstitution isectElimination universeEquality sqequalRule lambdaEquality functionEquality cumulativity hypothesisEquality because_Cache functionExtensionality applyEquality hypothesis dependent_set_memberEquality natural_numberEquality dependent_functionElimination unionElimination independent_pairFormation voidElimination productElimination independent_functionElimination independent_isectElimination addEquality isect_memberEquality voidEquality intEquality minusEquality Error :isect_memberFormation_alt,  axiomEquality Error :inhabitedIsType,  Error :functionIsType,  Error :universeIsType,  baseApply closedConclusion baseClosed equalityTransitivity equalitySymmetry dependent_pairFormation productEquality equalityElimination

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}[T:Type].  \mforall{}[R1,R2:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    (R1  =>  R2  {}\mRightarrow{}  rel\_exp(T;  R1;  n)  =>  rel\_exp(T;  R2;  n))



Date html generated: 2019_06_20-PM-00_30_27
Last ObjectModification: 2018_09_26-PM-00_49_25

Theory : relations


Home Index