apply_mem_iff — Mathlib

English

If a permutation f is cycle-on s, then membership is preserved by f: f(x) ∈ s iff x ∈ s. More precisely, for hf : f.IsCycleOn s, f x ∈ s ↔ x ∈ s.

Русский

Если f образует цикл на s, то принадлежность сохраняется: f(x) ∈ s эквивалентно x ∈ s.

LaTeX

$$$\mathrm{IsCycleOn}(f,s) \Rightarrow (f(x) \in s \iff x \in s)$$$

Lean4

theorem apply_mem_iff (hf : f.IsCycleOn s) : f x ∈ s ↔ x ∈ s :=
  ⟨fun hx => by
    convert hf.1.perm_inv.1 hx
    rw [inv_apply_self], fun hx => hf.1.mapsTo hx⟩

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