map_balance — Mathlib

English

Let g be a linear map between modules. Then applying g to balance f at a is the same as taking balance of g∘f at a: g(balance f(a)) = balance(g ∘ f)(a).

Русский

Пусть g — линейное отображение; тогда g(balance f(a)) = balance(g ∘ f)(a).

LaTeX

$$$$ g\\big(\\mathrm{balance}(f)(a)\\big) = \\mathrm{balance}(g \\circ f)(a). $$$$

Lean4

@[simp]
theorem map_balance [FunLike F G H] [LinearMapClass F ℚ≥0 G H] (g : F) (f : ι → G) (a : ι) :
    g (balance f a) = balance (g ∘ f) a := by simp [balance, map_expect]

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