mul_swap_eq_iff — Mathlib

English

Let α be a set with decidable equality, σ a permutation of α, and i, j ∈ α. Then σ ∘ (i j) = σ if and only if i = j.

Русский

Пусть α — множество с разрешяемым равенством, σ — перестановка α, и i, j ∈ α. Тогда σ ∘ (i j) = σ тогда и только тогда, когда i = j.

LaTeX

$$$\\\\forall i,j \\\\in \\\\alpha, \\\\forall \\\\sigma \\\\in \\\\mathrm{Perm}(\\\\alpha): \\\\sigma \circ (i \\\\ j) = \\\\sigma \\\\iff i = j.$$$

Lean4

theorem mul_swap_eq_iff {i j : α} {σ : Perm α} : σ * swap i j = σ ↔ i = j := by rw [mul_eq_left, swap_eq_one_iff]

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