cycleOf_eq — Mathlib

English

If f is a cycle and x is not fixed, then cycleOf f x equals f; if x is fixed, cycleOf f x equals 1.

Русский

Если f — цикл и x не зафиксирован, то cycleOf f x = f; иначе cycleOf f x = 1.

LaTeX

$$cycleOf_eq [DecidableRel f.SameCycle] (hf : IsCycle f) (hx : f x ≠ x) : cycleOf f x = f$$

Lean4

theorem cycleOf_eq [DecidableRel f.SameCycle] (hf : IsCycle f) (hx : f x ≠ x) : cycleOf f x = f :=
  Equiv.ext fun y =>
    if h : SameCycle f x y then by rw [h.cycleOf_apply]
    else by rw [cycleOf_apply_of_not_sameCycle h, Classical.not_not.1 (mt ((isCycle_iff_sameCycle hx).1 hf).2 h)]

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