swap_mem_trans — Mathlib

English

If swap a b and swap b c belong to a submonoid M of Perm α, then swap a c also lies in M.

Русский

Если транспозиции swap a b и swap b c принадлежат подмоноиду M перестановок на α, то и swap a c принадлежит M.

LaTeX

$$$$ swap\\ a\\ c \\in M $$$$

Lean4

theorem swap_mem_trans {a b c : α} {C} [SetLike C (Perm α)] [SubmonoidClass C (Perm α)] (M : C) (hab : swap a b ∈ M)
    (hbc : swap b c ∈ M) : swap a c ∈ M := by
  obtain rfl | hab' := eq_or_ne a b
  · exact hbc
  obtain rfl | hac := eq_or_ne a c
  · exact swap_self a ▸ one_mem M
  rw [swap_comm, ← swap_mul_swap_mul_swap hab' hac]
  exact mul_mem (mul_mem hbc hab) hbc

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