mem_support_iff — Mathlib

English

For f an equivalence permutation, y lies in the support of f.cycleOf x iff x and y are in the same cycle and x lies in the support of f.

Русский

Для эквивалентной перестановки y∈support(f.cycleOf x) эквивалентно тому, что x и y лежат в одном цикле и x лежит в поддержке f.

LaTeX

$$$y \\\\in \\\\mathrm{support}(f.\\\\cycleOf x) \\\\iff (f.SameCycle x y) \\\\land x \\\\in \\\\mathrm{support} f$$$

Lean4

theorem mem_support_iff {f} [DecidableEq α] [Fintype α] (h : SameCycle f x y) : x ∈ support f ↔ y ∈ support f :=
  ⟨fun hx => support_cycleOf_le f x (mem_support_cycleOf_iff.mpr ⟨h, hx⟩), fun hy =>
    support_cycleOf_le f y (mem_support_cycleOf_iff.mpr ⟨h.symm, hy⟩)⟩

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