Nuprl Definition : onto-map

This says that relation R maps A onto B. ⋅

R:(A ─>> B) == ∀y:coSet{i:l}. ((y ∈ B) ⇒ (∃x:coSet{i:l}. ((x ∈ A) ∧ (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 : onto-map

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