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
.