English
If v i = v j, then v(sw ap i j k) = v(k) for all k; i.e., v is invariant under the swap when its values at i and j coincide.
Русский
Если v(i) = v(j), то v( swap(i,j)(k) ) = v(k) для всех k; то есть v инвариантна относительно перестановки, когда значения в i и j совпадают.
LaTeX
$$$(v(i) = v(j)) \Rightarrow \forall k, \, v(\mathrm{swap}(i,j)(k)) = v(k)$$$
Lean4
/-- A function is invariant to a swap if it is equal at both elements -/
theorem apply_swap_eq_self {v : α → β} {i j : α} (hv : v i = v j) (k : α) : v (swap i j k) = v k :=
by
by_cases hi : k = i
· rw [hi, swap_apply_left, hv]
by_cases hj : k = j
· rw [hj, swap_apply_right, hv]
rw [swap_apply_of_ne_of_ne hi hj]
