ofReal_balance — Mathlib

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 ..) ..

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