English
If a ∈ s but b ∉ s, swapping a and b yields a bijection from s onto insert(b, s \\ {a}).
Русский
Если a ∈ s, а b ∉ s, перестановка a и b задает биекцию s → insert(b, s \\ {a}).
LaTeX
$$BijOn (Equiv.swap a b) s (insert b (s \\ { a }))$$
Lean4
theorem swap_bijOn_exchange (ha : a ∈ s) (hb : b ∉ s) : BijOn (Equiv.swap a b) s (insert b (s \ { a })) :=
by
refine ⟨fun x hx ↦ ?_, (Equiv.injective _).injOn, fun x hx ↦ ?_⟩
· obtain (rfl | hxa) := eq_or_ne x a
· simp [swap_apply_left]
rw [swap_apply_of_ne_of_ne hxa (by rintro rfl; contradiction)]
exact .inr ⟨hx, hxa⟩
obtain (rfl | hxb) := eq_or_ne x b
· exact ⟨a, ha, by simp⟩
simp only [mem_insert_iff, mem_diff, mem_singleton_iff, or_iff_right hxb] at hx
exact ⟨x, hx.1, swap_apply_of_ne_of_ne hx.2 hxb⟩
