Commit 2024-05-14 15:22 b1087dd1

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.