swap_eq_refl_iff — Mathlib

English

The swap equals the identity if and only if the two elements are equal.

Русский

Перестановка swap(a,b) равна тождественной тогда и только тогда, когда a = b.

LaTeX

$$$\mathrm{swap}(x,y) = \mathrm{id} \iff x = y$$$

Lean4

@[simp]
theorem swap_eq_refl_iff {x y : α} : swap x y = Equiv.refl _ ↔ x = y :=
  by
  refine ⟨fun h => (Equiv.refl _).injective ?_, fun h => h ▸ swap_self _⟩
  rw [← h, swap_apply_left, h, refl_apply]

Похожие утверждения