swap_apply_ne_self_iff — Mathlib

English

The swap moves x if and only if a ≠ b and (x = a or x = b).

Русский

Перестановка swap перемещает x тогда, когда a ≠ b и (x = a или x = b).

LaTeX

$$$\mathrm{swap}(a,b)(x) \neq x \iff a \neq b \land (x = a \lor x = b)$$$

Lean4

theorem swap_apply_ne_self_iff {a b x : α} : swap a b x ≠ x ↔ a ≠ b ∧ (x = a ∨ x = b) :=
  by
  by_cases hab : a = b
  · simp [hab]
  by_cases hax : x = a
  · simp [hax, eq_comm]
  by_cases hbx : x = b
  · simp [hbx]
  simp [hab, hax, hbx, swap_apply_of_ne_of_ne]

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