balance_idem — Mathlib

English

Applying balance twice is the same as applying balance once: balance(balance(f)) = balance(f).

Русский

Применение баланса дважды равно одному разу: balance(balance(f)) = balance(f).

LaTeX

$$$$ \\mathrm{balance}(\\mathrm{balance}(f)) = \\mathrm{balance}(f). $$$$

Lean4

@[simp]
theorem balance_idem (f : ι → G) : balance (balance f) = balance f := by
  cases isEmpty_or_nonempty ι <;> ext x <;> simp [balance, expect_sub_distrib, univ_nonempty]

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