Definition 1.5.28. Let *X*, *Y* be sets. We define:

(*X* ↔ *Y*) := {*f* : *X* → *Y* : *f* is bijective}

We write “let *f* : *X* ↔ *Y* be a bijection” for “let *f* ∈ (*X* ↔ *Y*).”

Remarks.

Bijections are important enough to warrant their own notation. A bidirectional arrow seems appropriate, even though it does not appear to be standard.

References.