isCycleOn_singleton — Mathlib

English

For a finite β and a cycle f, f^a = f^b iff there exists a moved point x with f^a x = f^b x and f x ≠ x.

Русский

Для цикла f в конечном β, f^a = f^b тогда и только тогда, когда существует перемещаемая точка x с f^a x = f^b x и f x ≠ x.

LaTeX

$$$\\forall f : \\mathrm{Equiv.Perm}(\\beta),\\; \\mathrm{IsCycle}(f) \\Rightarrow \\forall a,b : \\mathrm{Nat},\\; \\mathrm{Eq}( \\mathrm{instHPow.hPow} f a, \\mathrm{instHPow.hPow} f b) \\Rightarrow \\exists x, f x \\neq x \\land \\mathrm{Eq}( \\mathrm{instHPow.hPow} f a x, \\mathrm{instHPow.hPow} f b x).$$$

Lean4

@[simp]
theorem isCycleOn_singleton : f.IsCycleOn { a } ↔ f a = a := by simp [IsCycleOn, SameCycle.rfl]

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