support_cycleOf_nonempty — Mathlib

English

The cycle of x under f has nonempty support exactly when x is moved by f.

Русский

Поддержка цикла x для f непустая тогда и только тогда, когда x не зафиксирован f.

LaTeX

$$$cycleOf f x\\\\.support \\\\neq \\\\emptyset \\\\iff f x \\\\neq x$$$

Lean4

@[simp]
theorem support_cycleOf_nonempty [DecidableEq α] [Fintype α] : (cycleOf f x).support.Nonempty ↔ f x ≠ x :=
  by
  rw [← two_le_card_support_cycleOf_iff, ← card_pos, ← Nat.succ_le_iff]
  exact ⟨fun h => Or.resolve_left h.eq_or_lt (card_support_ne_one _).symm, zero_lt_two.trans_le⟩

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