Nuprl Definition : lifting2-like

lifting2-like(A;B;f) ==
  (∀as:bag(A). ∀bs:bag(B). ∀a:A. ∀b:B.
     (single-valued-bag(as;A)
     ⇒ single-valued-bag(bs;B)
     ⇒ a ↓∈ as
     ⇒ b ↓∈ bs
     ⇒ (↑bag-null(f as bs) ⇐⇒ ↑bag-null(f {a} {b}))))
  ∧ (∀as:bag(A). (↑bag-null(f as {})))
  ∧ (∀bs:bag(B). (↑bag-null(f {} bs)))

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 : lifting2-like

Latex:
lifting2-like(A;B;f) == (\mforall{}as:bag(A). \mforall{}bs:bag(B). \mforall{}a:A. \mforall{}b:B. (single-valued-bag(as;A) {}\mRightarrow{} single-valued-bag(bs;B) {}\mRightarrow{} a \mdownarrow{}\mmember{} as {}\mRightarrow{} b \mdownarrow{}\mmember{} bs {}\mRightarrow{} (\muparrow{}bag-null(f as bs) \mLeftarrow{}{}\mRightarrow{} \muparrow{}bag-null(f \{a\} \{b\})))) \mwedge{} (\mforall{}as:bag(A). (\muparrow{}bag-null(f as \{\}))) \mwedge{} (\mforall{}bs:bag(B). (\muparrow{}bag-null(f \{\} bs))) Date html generated: 2015_07_23-AM-11_26_46 Last ObjectModification: 2012_08_27-PM-06_14_49 Home Index