re_balance — Mathlib

English

For a finite index set, balance f a is a real number; its real part equals the balance of the real parts: Re(balance f a) = balance (Re ∘ f) a.

Русский

Для конечного набора индексов значение balance f a есть вещественное число; его действительная часть равна балансу действительных частей: Re(balance f a) = balance (Re ∘ f) a.

LaTeX

$$$$ \operatorname{Re}\big( \operatorname{balance} f a \big) = \operatorname{balance} (\operatorname{Re} \circ f) a $$$$

Lean4

@[simp]
theorem re_balance [Fintype α] (f : α → ℂ) (a : α) : re (balance f a) = balance (re ∘ f) a := by simp [balance]

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