Nuprl Definition : fpf-sub
f ⊆ g == ∀x:A. ((↑x ∈ dom(f))
⇒ ((↑x ∈ dom(g)) c∧ (f(x) = g(x) ∈ B[x])))
Definitions occuring in Statement :
fpf-ap: f(x)
,
fpf-dom: x ∈ dom(f)
,
assert: ↑b
,
cand: A c∧ B
,
all: ∀x:A. B[x]
,
implies: P
⇒ Q
,
equal: s = t ∈ T
FDL editor aliases :
fpf-sub
f \msubseteq{} g == \mforall{}x:A. ((\muparrow{}x \mmember{} dom(f)) {}\mRightarrow{} ((\muparrow{}x \mmember{} dom(g)) c\mwedge{} (f(x) = g(x))))
Date html generated:
2015_07_17-AM-09_17_05
Last ObjectModification:
2012_02_25-AM-11_06_46
Home
Index