ofReal_comp_balance — Mathlib

English

For any finite index set, composing balance with the real embedding commutes with balance of the composed real-valued function, i.e., ofReal ∘ balance f = balance (ofReal ∘ f).

Русский

Для любого конечного множества индексов композиция вложения вещественных чисел в комплексные числа с балансом равна балансу после композиции функции: ofReal ∘ balance f = balance (ofReal ∘ f).

LaTeX

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

Lean4

@[simp]
theorem ofReal_comp_balance {ι : Type*} [Fintype ι] (f : ι → ℝ) : ofReal ∘ balance f = balance (ofReal ∘ f : ι → ℂ) :=
  funext <| ofReal_balance _

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