two_le_card_support_cycleOf_iff — Mathlib

English

The size of the support of cycleOf x has at least two elements if and only if f(x) ≠ x.

Русский

Размер множества поддержки cycleOf x не меньше двух тогда и только тогда, когда f(x) ≠ x.

LaTeX

$$$2 \\\\le |\\\\,(cycleOf f x).\\\\support| \\\\iff f(x) \\\\neq x$$$

Lean4

@[simp]
theorem two_le_card_support_cycleOf_iff [DecidableEq α] [Fintype α] : 2 ≤ #(cycleOf f x).support ↔ f x ≠ x :=
  by
  refine ⟨fun h => ?_, fun h => by simpa using (isCycle_cycleOf _ h).two_le_card_support⟩
  contrapose! h
  rw [← cycleOf_eq_one_iff] at h
  simp [h]

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