commute — Mathlib

English

If two permutations are disjoint, they commute.

Русский

Если две перестановки раздельны, они commute.

LaTeX

$$$\operatorname{Disjoint}(f,g) \rightarrow \operatorname{Commute}(f,g)$$$

Lean4

theorem commute (h : Disjoint f g) : Commute f g :=
  Equiv.ext fun x =>
    (h x).elim
      (fun hf =>
        (h (g x)).elim (fun hg => by simp [mul_apply, hf, hg]) fun hg => by simp [mul_apply, hf, g.injective hg])
      fun hg => (h (f x)).elim (fun hf => by simp [mul_apply, f.injective hf, hg]) fun hf => by simp [mul_apply, hf, hg]

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