English
If hs: a ∈ s ↔ b ∈ s, then swapping a and b restricts to a bijection s → s.
Русский
Если a и b либо оба принадлежат s, либо оба не принадлежат s, тогда перестановка a и b ограничена на s и образует биекцию s → s.
LaTeX
$$BijOn (Equiv.swap a b) s s$$
Lean4
theorem swap_bijOn_self (hs : a ∈ s ↔ b ∈ s) : BijOn (Equiv.swap a b) s s :=
by
refine ⟨fun x hx ↦ ?_, (Equiv.injective _).injOn, fun x hx ↦ ?_⟩
· obtain (rfl | hxa) := eq_or_ne x a
· rwa [swap_apply_left, ← hs]
obtain (rfl | hxb) := eq_or_ne x b
· rwa [swap_apply_right, hs]
rwa [swap_apply_of_ne_of_ne hxa hxb]
obtain (rfl | hxa) := eq_or_ne x a
· simp [hs.1 hx]
obtain (rfl | hxb) := eq_or_ne x b
· simp [hs.2 hx]
exact ⟨x, hx, swap_apply_of_ne_of_ne hxa hxb⟩
