# Commit 2024-05-14 15:22 b1087dd1

View on Github →feat(Logic/Equiv/Set): `swap`

is `BijOn`

(#12877)
We prove two lemmas, stating that `Equiv.swap a b`

is `BijOn s t`

, where `t = s`

if both or neither `a`

or `b`

belong to `s`

, and `t = s - a + b`

if `a ∈ s`

and `b ∉ s`

.