Nuprl Lemma : es-causle-retraction

es:EO. ∀[T:Type]. ∀f:T ─→ T. ((∀x:T. c≤ x)  retraction(T;f)) supposing strong-subtype(T;E)


Proof




Definitions occuring in Statement :  es-causle: c≤ e' es-E: E event_ordering: EO strong-subtype: strong-subtype(A;B) uimplies: supposing a uall: [x:A]. B[x] all: x:A. B[x] implies:  Q apply: a function: x:A ─→ B[x] universe: Type retraction: retraction(T;f)
Lemmas :  strong-subtype_witness es-E_wf all_wf es-causle_wf strong-subtype_wf event_ordering_wf es-causl-swellfnd subtype_rel_dep_function nat_wf subtype_rel_self or_wf equal_wf less_than_wf strong-subtype-implies
\mforall{}es:EO.  \mforall{}[T:Type].  \mforall{}f:T  {}\mrightarrow{}  T.  ((\mforall{}x:T.  f  x  c\mleq{}  x)  {}\mRightarrow{}  retraction(T;f))  supposing  strong-subtype(T;E)



Date html generated: 2015_07_17-AM-08_38_38
Last ObjectModification: 2015_01_27-PM-02_42_57

Home Index