Nuprl Definition : fpf-contains
f ⊆⊆ g == ∀x:A. ((↑x ∈ dom(f)) ⇒ ((↑x ∈ dom(g)) c∧ f(x) ⊆ g(x)))
Definitions occuring in Statement :
fpf-ap: f(x),
fpf-dom: x ∈ dom(f),
l_contains: A ⊆ B,
assert: ↑b,
cand: A c∧ B,
all: ∀x:A. B[x],
implies: P ⇒ Q
Definitions occuring in definition :
all: ∀x:A. B[x],
implies: P ⇒ Q,
cand: A c∧ B,
assert: ↑b,
fpf-dom: x ∈ dom(f),
l_contains: A ⊆ B,
fpf-ap: f(x)
FDL editor aliases :
fpf-contains
Latex:
f \msubseteq{}\msubseteq{} g == \mforall{}x:A. ((\muparrow{}x \mmember{} dom(f)) {}\mRightarrow{} ((\muparrow{}x \mmember{} dom(g)) c\mwedge{} f(x) \msubseteq{} g(x)))
Date html generated:
2018_05_21-PM-09_19_11
Last ObjectModification:
2018_02_09-AM-10_17_27
Theory : finite!partial!functions
Home
Index