Nuprl Lemma : Q-R-pre-preserving_functionality_wrt_implies

es:EO
  ∀[P1,P2:E ⟶ ℙ]. ∀[Q1,R1,Q2,R2:E ⟶ E ⟶ ℙ].
    ∀f:{e:E| P1 e}  ⟶ E
      (P1  P2  Q1  Q2  R1 => R2  {f is Q1-R1-pre-preserving on P1  is Q2-R2-pre-preserving on P2})


Proof




Definitions occuring in Statement :  Q-R-pre-preserving: is Q-R-pre-preserving on P es-E: E event_ordering: EO predicate_rev_implies: P1  P2 rel_rev_implies: R1  R2 rel_implies: R1 => R2 uall: [x:A]. B[x] prop: guard: {T} all: x:A. B[x] exists: x:A. B[x] implies:  Q set: {x:A| B[x]}  apply: a function: x:A ⟶ B[x] equal: t ∈ T
Definitions unfolded in proof :  Q-R-pre-preserving: is Q-R-pre-preserving on P guard: {T} rel_implies: R1 => R2 rel_rev_implies: R1  R2 predicate_rev_implies: P1  P2 infix_ap: y predicate_implies: P1  P2 all: x:A. B[x] uall: [x:A]. B[x] implies:  Q member: t ∈ T prop: subtype_rel: A ⊆B so_lambda: λ2x.t[x] so_apply: x[s] uimplies: supposing a exists: x:A. B[x]

Latex:
\mforall{}es:EO
    \mforall{}[P1,P2:E  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[Q1,R1,Q2,R2:E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}].
        \mforall{}f:\{e:E|  P1  e\}    {}\mrightarrow{}  E
            (P1  \mLeftarrow{}{}  P2
            {}\mRightarrow{}  Q1  \mLeftarrow{}{}  Q2
            {}\mRightarrow{}  R1  =>  R2
            {}\mRightarrow{}  \{f  is  Q1-R1-pre-preserving  on  P1  {}\mRightarrow{}  f  is  Q2-R2-pre-preserving  on  P2\})



Date html generated: 2016_05_16-AM-10_18_40
Last ObjectModification: 2015_12_28-PM-09_25_16

Theory : new!event-ordering


Home Index