cycleOf_apply — Mathlib

English

The cycleOf f x y equals f y if x and y lie in the same cycle of f; otherwise it fixes y.

Русский

Функция cycleOf f x действует на y как f y, если x и y лежат в одной цепи цикла f; иначе она фиксирует y.

LaTeX

$$$ cycleOf f x y = \\begin{cases} f y, & \\text{if } SameCycle f x y; \\\\ y, & \\text{otherwise}. \\end{cases}$$$$

Lean4

theorem cycleOf_apply (f : Perm α) [DecidableRel f.SameCycle] (x y : α) :
    cycleOf f x y = if SameCycle f x y then f y else y :=
  by
  dsimp only [cycleOf]
  split_ifs with h
  · apply ofSubtype_apply_of_mem
    exact h
  · apply ofSubtype_apply_of_not_mem
    exact h

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