card_support_le_one — Mathlib

English

The support of f has size at most 1 if and only if f is the identity.

Русский

Опора перестановки имеет размер не более единицы тогда и только тогда, когда она тождественна.

LaTeX

$$$\#f.\operatorname{support} \le 1 \iff f = 1$$$

Lean4

@[simp]
theorem card_support_le_one {f : Perm α} : #f.support ≤ 1 ↔ f = 1 := by
  rw [le_iff_lt_or_eq, Nat.lt_succ_iff, Nat.le_zero, card_support_eq_zero, or_iff_not_imp_right,
    imp_iff_right f.card_support_ne_one]

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