### Nuprl Lemma : fpf-sub-functionality

`∀[A,A':Type].`
`  ∀[B:A ─→ Type]. ∀[C:A' ─→ Type]. ∀[eq:EqDecider(A)]. ∀[eq':EqDecider(A')]. ∀[f,g:a:A fp-> B[a]].`
`    (f ⊆ g) supposing (f ⊆ g and (∀a:A. (B[a] ⊆r C[a]))) `
`  supposing strong-subtype(A;A')`

Proof

Definitions occuring in Statement :  fpf-sub: `f ⊆ g` fpf: `a:A fp-> B[a]` deq: `EqDecider(T)` strong-subtype: `strong-subtype(A;B)` uimplies: `b supposing a` subtype_rel: `A ⊆r B` uall: `∀[x:A]. B[x]` so_apply: `x[s]` all: `∀x:A. B[x]` function: `x:A ─→ B[x]` universe: `Type`
Lemmas :  strong-subtype-implies assert_wf fpf-dom_wf subtype_rel-deq equal_wf subtype-fpf2 top_wf subtype_top fpf-sub_witness fpf-sub_wf all_wf subtype_rel_wf fpf_wf deq_wf strong-subtype_wf fpf-dom_functionality2 fpf-ap_wf
\mforall{}[A,A':Type].
\mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[C:A'  {}\mrightarrow{}  Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[eq':EqDecider(A')].  \mforall{}[f,g:a:A  fp->  B[a]].
(f  \msubseteq{}  g)  supposing  (f  \msubseteq{}  g  and  (\mforall{}a:A.  (B[a]  \msubseteq{}r  C[a])))
supposing  strong-subtype(A;A')

Date html generated: 2015_07_17-AM-09_17_23
Last ObjectModification: 2015_01_28-AM-07_59_56

Home Index