### Nuprl Lemma : rel_plus-weak-TI

`∀T:Type. ∀R:T ⟶ T ⟶ ℙ.  (∀Q:T ⟶ ℙ. weak-TI(T;x,y.R[x;y];x.Q[x]) `⇐⇒` ∀Q:T ⟶ ℙ. weak-TI(T;x,y.R+ x y;x.Q[x]))`

Proof

Definitions occuring in Statement :  rel_plus: `R+` weak-TI: `weak-TI(T;x,y.R[x; y];t.Q[t])` prop: `ℙ` so_apply: `x[s1;s2]` so_apply: `x[s]` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` apply: `f a` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` implies: `P `` Q` member: `t ∈ T` prop: `ℙ` uall: `∀[x:A]. B[x]` so_lambda: `λ2x.t[x]` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` so_apply: `x[s]` rev_implies: `P `` Q` subtype_rel: `A ⊆r B` weak-TI: `weak-TI(T;x,y.R[x; y];t.Q[t])` cand: `A c∧ B` guard: `{T}` infix_ap: `x f y` exists: `∃x:A. B[x]` or: `P ∨ Q`
Lemmas referenced :  all_wf weak-TI_wf rel_plus_wf rel_plus_iff2 rel-star-iff-rel-plus and_wf equal_wf rel-rel-plus
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation independent_pairFormation functionEquality cumulativity hypothesisEquality universeEquality cut thin instantiate introduction extract_by_obid sqequalHypSubstitution isectElimination sqequalRule lambdaEquality applyEquality functionExtensionality hypothesis because_Cache dependent_functionElimination productEquality independent_functionElimination productElimination unionElimination dependent_set_memberEquality setElimination rename setEquality equalitySymmetry hyp_replacement Error :applyLambdaEquality

Latex:
\mforall{}T:Type.  \mforall{}R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}.
(\mforall{}Q:T  {}\mrightarrow{}  \mBbbP{}.  weak-TI(T;x,y.R[x;y];x.Q[x])  \mLeftarrow{}{}\mRightarrow{}  \mforall{}Q:T  {}\mrightarrow{}  \mBbbP{}.  weak-TI(T;x,y.R\msupplus{}  x  y;x.Q[x]))

Date html generated: 2016_10_21-AM-10_50_06
Last ObjectModification: 2016_07_12-AM-05_54_17

Theory : relations2

Home Index