Nuprl Lemma : rel_plus_idempotent

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


Proof




Definitions occuring in Statement :  rel_plus: R+ uall: [x:A]. B[x] prop: all: x:A. B[x] iff: ⇐⇒ Q apply: a function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] all: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q implies:  Q member: t ∈ T prop: rev_implies:  Q rel_plus: R+ rel_implies: R1 => R2 infix_ap: 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 ⊆B rel_exp: R^n eq_int: (i =z j) subtract: m ifthenelse: if then else fi  bfalse: ff cand: 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