English
The embedding of balance f at i coincides with the balance of the embedded function: ofReal(balance f i) = balance((↑) ∘ f) i.
Русский
Встраивание баланса сохраняется: ofReal(balance f i) = balance((↑) ∘ f) i.
LaTeX
$$$\operatorname{ofReal}(\operatorname{balance} f i) = \operatorname{balance}(\operatorname{ofReal} \circ f) i$$$
Lean4
@[norm_cast]
theorem ofReal_balance {ι : Type*} [Fintype ι] (f : ι → ℝ) (i : ι) : ((balance f i : ℝ) : K) = balance ((↑) ∘ f) i :=
map_balance (algebraMap ..) ..