one_lt_card_support_of_ne_one — Mathlib

English

If a permutation f is not the identity, then its support contains more than one element.

Русский

Если перестановка f не тождественна, то её опора содержит более одного элемента.

LaTeX

$$$f \neq 1 \Rightarrow 1 < \#f.\operatorname{support}$$$

Lean4

theorem one_lt_card_support_of_ne_one {f : Perm α} (h : f ≠ 1) : 1 < #f.support :=
  by
  simp_rw [one_lt_card_iff, mem_support, ← not_or]
  contrapose! h
  ext a
  specialize h (f a) a
  rwa [apply_eq_iff_eq, or_self_iff, or_self_iff] at h

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