Nuprl Lemma : fpf-dom-type

[X,Y:Type]. ∀[eq:EqDecider(Y)]. ∀[f:x:X fp-> Top]. ∀[x:Y].  (x ∈ X) supposing ((↑x ∈ dom(f)) and strong-subtype(X;Y))


Definitions occuring in Statement :  fpf-dom: x ∈ dom(f) fpf: a:A fp-> B[a] deq: EqDecider(T) strong-subtype: strong-subtype(A;B) assert: b uimplies: supposing a uall: [x:A]. B[x] top: Top member: t ∈ T universe: Type
Lemmas :  strong-subtype-l_member-type fpf-domain_wf member-fpf-domain assert_wf fpf-dom_wf subtype-fpf3 top_wf subtype_rel_self strong-subtype_wf fpf_wf deq_wf
\mforall{}[X,Y:Type].  \mforall{}[eq:EqDecider(Y)].  \mforall{}[f:x:X  fp->  Top].  \mforall{}[x:Y].
    (x  \mmember{}  X)  supposing  ((\muparrow{}x  \mmember{}  dom(f))  and  strong-subtype(X;Y))

Date html generated: 2015_07_17-AM-09_16_00
Last ObjectModification: 2015_01_28-AM-07_52_31

Home Index