destutter_idem — Mathlib

English

destutter is idempotent: applying destutter twice yields the same as applying it once.

Русский

destutter идемпотентен: повторное применение дает тот же результат, что и первое.

LaTeX

$$$$\operatorname{destutter}(\operatorname{destutter}(l)) = \operatorname{destutter}(l).$$$$

Lean4

theorem destutter_idem : (l.destutter R).destutter R = l.destutter R :=
  destutter_of_isChain R _ <| l.isChain_destutter R

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