### Nuprl Lemma : rel_plus_idempotent

`∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀x,y:T.  (R+ x y `⇐⇒` R++ x y)`

Proof

Definitions occuring in Statement :  rel_plus: `R+` uall: `∀[x:A]. B[x]` prop: `ℙ` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` apply: `f a` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` implies: `P `` Q` member: `t ∈ T` prop: `ℙ` rev_implies: `P `` Q` rel_plus: `R+` rel_implies: `R1 => R2` infix_ap: `x f y` exists: `∃x:A. B[x]` nat_plus: `ℕ+` less_than: `a < b` squash: `↓T` less_than': `less_than'(a;b)` true: `True` subtype_rel: `A ⊆r B` rel_exp: `R^n` eq_int: `(i =z j)` subtract: `n - m` ifthenelse: `if b then t else f fi ` bfalse: `ff` cand: `A c∧ B` nat: `ℕ` le: `A ≤ B` false: `False` not: `¬A` btrue: `tt`
Lemmas referenced :  rel_plus_trans rel_plus_minimal le_wf false_wf infix_ap_wf nat_plus_subtype_nat rel_exp_wf less_than_wf rel_plus_monotone rel_plus_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation independent_pairFormation applyEquality cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality sqequalRule hypothesis functionEquality cumulativity universeEquality independent_functionElimination dependent_pairFormation dependent_set_memberEquality natural_numberEquality introduction imageMemberEquality baseClosed productEquality instantiate because_Cache dependent_functionElimination

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

Date html generated: 2016_05_14-PM-03_55_18
Last ObjectModification: 2016_01_14-PM-11_10_44

Theory : relations2

Home Index