Nuprl Lemma : subtype-fpf-cap-top

[T,X:Type]. ∀[eq:EqDecider(X)]. ∀[f,g:x:X fp-> Type]. ∀[x:X].  f(x)?T ⊆g(x)?Top supposing g ⊆ f


Proof




Definitions occuring in Statement :  fpf-sub: f ⊆ g fpf-cap: f(x)?z fpf: a:A fp-> B[a] deq: EqDecider(T) uimplies: supposing a subtype_rel: A ⊆B uall: [x:A]. B[x] top: Top universe: Type
Lemmas :  fpf-ap_wf subtype_rel_wf
\mforall{}[T,X:Type].  \mforall{}[eq:EqDecider(X)].  \mforall{}[f,g:x:X  fp->  Type].  \mforall{}[x:X].    f(x)?T  \msubseteq{}r  g(x)?Top  supposing  g  \msubseteq{}  f



Date html generated: 2015_07_17-AM-09_17_52
Last ObjectModification: 2015_01_28-AM-07_51_05

Home Index