card_support_swap_mul — Mathlib

English

If f moves x (i.e., f(x) ≠ x), then the support of the permutation swap x with f(x) multiplied by f is strictly smaller than the support of f.

Русский

Если f движет x, то опора перестановки swap x f(x) · f меньше опоры f.

LaTeX

$$$(f(x) \neq x) \Rightarrow \#\operatorname{supp}(\operatorname{swap}(x, f(x)) \cdot f) < \#\operatorname{supp}(f)$$$

Lean4

theorem card_support_swap_mul {f : Perm α} {x : α} (hx : f x ≠ x) : #(swap x (f x) * f).support < #f.support :=
  Finset.card_lt_card
    ⟨fun _ hz => (mem_support_swap_mul_imp_mem_support_ne hz).left, fun h =>
      absurd (h (mem_support.2 hx)) (mt mem_support.1 (by simp))⟩

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