bijOn_swap — Mathlib

English

If a and b belong to s, then swapping them via swap a b yields a bijection of s onto itself.

Русский

Если a и b принадлежат s, перестановка swap(a,b) даёт биективное отображение s в s.

LaTeX

$$$(a \in s) \land (b \in s) \Rightarrow \mathrm{BijOn}(\mathrm{swap}(a,b), s, s)$$$

Lean4

theorem bijOn_swap (ha : a ∈ s) (hb : b ∈ s) : BijOn (swap a b) s s :=
  (swap a b).bijOn fun x ↦ by
    obtain rfl | hxa := eq_or_ne x a <;> obtain rfl | hxb := eq_or_ne x b <;> simp [*, swap_apply_of_ne_of_ne]

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