English
Let f: α → β be injective. For all x, y, z ∈ α, f(swap x y z) = swap(f(x)) (f(y)) (f(z)). In words, f preserves the swap of the three arguments.
Русский
Пусть f: α → β инъективно. Для любых x, y, z ∈ α выполняется f(перестановка x, y, z) = перестановка(f(x), f(y), f(z)). Иными словами, отображение сохраняет операцию перестановки тройки значений.
LaTeX
$$$\text{If } f:\alpha\to\beta\text{ is injective, then for all } x,y,z:\alpha, \ f(\mathrm{swap}\,x\,y\,z)=\mathrm{swap}\,(f(x))\,(f(y))\,(f(z)).$$$
Lean4
theorem map_swap [DecidableEq α] [DecidableEq β] {f : α → β} (hf : Function.Injective f) (x y z : α) :
f (Equiv.swap x y z) = Equiv.swap (f x) (f y) (f z) :=
by
conv_rhs => rw [Equiv.swap_apply_def]
split_ifs with h₁ h₂
· rw [hf h₁, Equiv.swap_apply_left]
· rw [hf h₂, Equiv.swap_apply_right]
· rw [Equiv.swap_apply_of_ne_of_ne (mt (congr_arg f) h₁) (mt (congr_arg f) h₂)]
