Nuprl Definition : mv-map

This says that the relation R relates every member of A
to at least one member of B. So it is a "multi-valued map" from A to B.⋅

R:(A ⇒ B) == ∀x:coSet{i:l}. ((x ∈ A) ⇒ (∃y:coSet{i:l}. ((y ∈ B) ∧ (R x y))))

Definitions occuring in Statement : setmem: (x ∈ s), coSet: coSet{i:l}, all: ∀x:A. B[x], exists: ∃x:A. B[x], implies: P ⇒ Q, and: P ∧ Q, apply: f a
Definitions occuring in definition : apply: f a, setmem: (x ∈ s), and: P ∧ Q, coSet: coSet{i:l}, exists: ∃x:A. B[x], implies: P ⇒ Q, all: ∀x:A. B[x]
FDL editor aliases : mv-map

Latex:
R:(A {}\mRightarrow{} B) == \mforall{}x:coSet\{i:l\}. ((x \mmember{} A) {}\mRightarrow{} (\mexists{}y:coSet\{i:l\}. ((y \mmember{} B) \mwedge{} (R x y)))) Date html generated: 2018_07_29-AM-10_06_13 Last ObjectModification: 2018_07_20-PM-00_56_48 Theory : constructive!set!theory Home Index