ofReal_balance — Mathlib

English

For a finite index set, balance f a is a real number; its image in ℂ equals the balance of the real-to-complex function at a.

Русский

Для конечного множества индексов баланс f a — вещественное число; его изображение в ℂ равно балансу функции f, встроенной в ℂ, в точке a.

LaTeX

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

Lean4

@[simp, norm_cast]
theorem ofReal_balance [Fintype α] (f : α → ℝ) (a : α) : ((balance f a : ℝ) : ℂ) = balance ((↑) ∘ f) a := by
  simp [balance]

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