cycleOf_eq — Mathlib

English

If x lies in the support of some cycle factor, then the Basis element a assigns to the pair (g.cycleOf x) the SameCycle relation with x.

Русский

Если x лежит в опоре цикл-фактора, то a связывает (g.cycleOf x) и x через отношение SameCycle.

LaTeX

$$For all x, if x ∈ support(g.cycleOf x) then g.SameCycle(a⟨g.cycleOf x, hx⟩) x$$

Lean4

theorem cycleOf_eq : g.cycleOf (a c) = c :=
  (cycle_is_cycleOf (a.mem_support_self c) c.prop).symm

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