Nuprl Definition : lifting-like
lifting-like(A;f) ==
(∀as:bag(A). ∀x:A. (single-valued-bag(as;A) ⇒ x ↓∈ as ⇒ (↑bag-null(f as) ⇐⇒ ↑bag-null(f {x}))))
∧ (↑bag-null(f {}))
Definitions occuring in Statement :
assert: ↑b,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
implies: P ⇒ Q,
and: P ∧ Q,
apply: f a,
single-valued-bag: single-valued-bag(b;T),
bag-member: x ↓∈ bs,
bag-null: bag-null(bs),
single-bag: {x},
empty-bag: {},
bag: bag(T)
FDL editor aliases :
lifting-like
Latex:
lifting-like(A;f) ==
(\mforall{}as:bag(A). \mforall{}x:A.
(single-valued-bag(as;A) {}\mRightarrow{} x \mdownarrow{}\mmember{} as {}\mRightarrow{} (\muparrow{}bag-null(f as) \mLeftarrow{}{}\mRightarrow{} \muparrow{}bag-null(f \{x\}))))
\mwedge{} (\muparrow{}bag-null(f \{\}))
Date html generated:
2015_07_23-AM-11_26_38
Last ObjectModification:
2012_08_27-AM-11_19_19
Home
Index