support_swap_mul_ge_support_diff — Mathlib

English

For permutations swap x y and swap y z, the support of their product equals {x,y,z} provided x,y,z are distinct.

Русский

Для перестановок swap x y и swap y z опора их произведения равна {x,y,z} при условии, что x,y,z различны.

LaTeX

$$$\operatorname{supp}(\operatorname{swap} x y \cdot \operatorname{swap} y z) = \{x,y,z\}$ при скрещивании условий на x,y,z (x≠y≠z).$$

Lean4

theorem support_swap_mul_ge_support_diff (f : Perm α) (x y : α) : f.support \ { x, y } ≤ (swap x y * f).support :=
  by
  intro
  simp only [and_imp, Perm.coe_mul, Function.comp_apply, Ne, mem_support, mem_insert, mem_sdiff, mem_singleton]
  push_neg
  rintro ha ⟨hx, hy⟩ H
  rw [swap_apply_eq_iff, swap_apply_of_ne_of_ne hx hy] at H
  exact ha H

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