idem — Mathlib

English

Applying reduction twice yields the same result as applying it once: reduce(reduce(L)) = reduce(L).

Русский

Повторное применение редукции эквивалентно одному: reduce(reduce(L)) = reduce(L).

LaTeX

$$$$\operatorname{reduce}(\operatorname{reduce}(L)) = \operatorname{reduce}(L).$$$$

Lean4

/-- `reduce` is idempotent, i.e. the maximal reduction of the maximal reduction of a word is the
  maximal reduction of the word. -/
@[to_additive (attr := simp) /-- `reduce` is idempotent, i.e. the maximal reduction of the maximal
      reduction of a word is the maximal reduction of the word. -/
    ]
theorem idem : reduce (reduce L) = reduce L :=
  Eq.symm <| reduce.min reduce.red

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