Nuprl Lemma : conditional-apply

[T,V:Type]. ∀[A,B:T ─→ ℙ]. ∀[dcd_A:t:T ─→ Dec(A t)]. ∀[f:{t:T| t}  ─→ V]. ∀[g:{t:T| t}  ─→ V]. ∀[t:{t:T| 
                                                                                                       (A t) ∨ (B t)} ].
  (([A? g] t) (f t) ∈ supposing t ∧ ([A? g] t) (g t) ∈ supposing ¬(A t))


Proof




Definitions occuring in Statement :  conditional: [P? g] decidable: Dec(P) uimplies: supposing a uall: [x:A]. B[x] prop: not: ¬A or: P ∨ Q and: P ∧ Q set: {x:A| B[x]}  apply: a function: x:A ─→ B[x] universe: Type equal: t ∈ T
Lemmas :  or_wf subtype_base_sq subtype_rel_sets decidable_wf equal_wf set_wf not_wf sq_stable_from_decidable
\mforall{}[T,V:Type].  \mforall{}[A,B:T  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[dcd$_{A}$:t:T  {}\mrightarrow{}  Dec(A  t)].  \mforall{}[f:\{t:T|  A  t\}    {}\mrightarrow{}  V].\000C  \mforall{}[g:\{t:T|  B  t\}    {}\mrightarrow{}  V].
\mforall{}[t:\{t:T|  (A  t)  \mvee{}  (B  t)\}  ].
    (([A?  f  :  g]  t)  =  (f  t)  supposing  A  t  \mwedge{}  ([A?  f  :  g]  t)  =  (g  t)  supposing  \mneg{}(A  t))



Date html generated: 2015_07_17-AM-09_01_39
Last ObjectModification: 2015_01_27-PM-00_55_55

Home Index