apply_ne — Mathlib

English

If f is a cycle on a set s, then for any nontrivial subset s, there exists a point a in s moved by f, hence f a ≠ a.

Русский

Если f — цикл на s, для любой нетривиальной подмножества найдется точка a, которая сдвигается f, то есть f a ≠ a.

LaTeX

$$$\\forall f:\\mathrm{Equiv.Perm}(\\alpha), \\forall s : \\mathrm{Set}(\\alpha), \\mathrm{IsCycleOn}(f,s) \\Rightarrow f a \\neq a \\text{ для некоторого } a \\in s.$$$

Lean4

protected theorem apply_ne (hf : f.IsCycleOn s) (hs : s.Nontrivial) (ha : a ∈ s) : f a ≠ a :=
  by
  obtain ⟨b, hb, hba⟩ := hs.exists_ne a
  obtain ⟨n, rfl⟩ := hf.2 ha hb
  exact fun h => hba (IsFixedPt.perm_zpow h n)

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