### Nuprl Lemma : conditional_wf2

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

Proof

Definitions occuring in Statement :  conditional: `[P? f : g]` decidable: `Dec(P)` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s]` or: `P ∨ Q` member: `t ∈ T` set: `{x:A| B[x]} ` lambda: `λx.A[x]` function: `x:A ─→ B[x]` universe: `Type`
Lemmas :  conditional_wf or_wf subtype_rel_dep_function decidable_wf subtype_rel_self set_wf subtype_rel_nested_set2 subtype_rel_sets not_wf
\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].
([\mlambda{}t.A[t]?  f  :  g]  \mmember{}  \{t:T|  A[t]  \mvee{}  B[t]\}    {}\mrightarrow{}  V)

Date html generated: 2015_07_17-AM-09_01_26
Last ObjectModification: 2015_01_27-PM-00_56_19

Home Index