Nuprl Definition : da-agrees
da-agrees(da;k.T[k]) == ∀k:Knd. ((↑k ∈ dom(da)) ⇒ T[k] ≡ da(k))
Definitions occuring in Statement :
fpf-ap: f(x),
fpf-dom: x ∈ dom(f),
Kind-deq: KindDeq,
Knd: Knd,
assert: ↑b,
ext-eq: A ≡ B,
all: ∀x:A. B[x],
implies: P ⇒ Q
FDL editor aliases :
da-agrees
da-agrees(da;k.T[k]) == \mforall{}k:Knd. ((\muparrow{}k \mmember{} dom(da)) {}\mRightarrow{} T[k] \mequiv{} da(k))
Date html generated:
2015_07_17-AM-11_19_07
Last ObjectModification:
2012_02_25-AM-11_16_00
Home
Index