Nuprl Definition : es-decl-sets-sub
dd1 ⊆ dd2 ==
let S1,ds1,da1 = dd1 in
let S2,ds2,da2 = dd2 in
∀i:Id. ((i ∈ S1) ⇒ ((i ∈ S2) ∧ da1 i ⊆ da2 i ∧ ds1 i ⊆ ds2 i))
Definitions occuring in Statement :
fpf-sub: f ⊆ g,
hasloc: hasloc(k;i),
Kind-deq: KindDeq,
Knd: Knd,
id-deq: IdDeq,
Id: Id,
l_member: (x ∈ l),
assert: ↑b,
spreadn: spread3,
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
universe: Type
FDL editor aliases :
es-decl-sets-sub
dd1 \msubseteq{} dd2 ==
let S1,ds1,da1 = dd1 in
let S2,ds2,da2 = dd2 in
\mforall{}i:Id. ((i \mmember{} S1) {}\mRightarrow{} ((i \mmember{} S2) \mwedge{} da1 i \msubseteq{} da2 i \mwedge{} ds1 i \msubseteq{} ds2 i))
Date html generated:
2015_07_17-AM-11_57_12
Last ObjectModification:
2013_03_27-AM-10_39_03
Home
Index