eq_or_eq_of_swap_apply_ne_self — Mathlib

English

If x ≠ a and x ≠ b, then swap a b x ≠ x implies x ∈ {a,b}. More generally, swap only moves a or b.

Русский

Если x ≠ a и x ≠ b, то swap a b x ≠ x означает, что x ∈ {a,b}. Иначе swap не меняет x.

LaTeX

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

Lean4

theorem eq_or_eq_of_swap_apply_ne_self {a b x : α} (h : swap a b x ≠ x) : x = a ∨ x = b :=
  by
  contrapose! h
  exact swap_apply_of_ne_of_ne h.1 h.2

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