norm_condExpInd_apply_le — Mathlib

English

For a general scalar c ∈ 𝕜 with SMul-commuting structure, condExpInd is linear in x with respect to c.

Русский

Для общего скаляра c ∈ 𝕜 при заданной структуре SMul-commutation condExpInd линейно по x.

LaTeX

$$$ condExpInd\; F\; hm\; \mu\; s\; (c \cdot x) = c \cdot condExpInd\; F\; hm\; \mu\; s\; x,$$

Lean4

theorem norm_condExpInd_apply_le (x : G) : ‖condExpInd G hm μ s x‖ ≤ μ.real s * ‖x‖ :=
  norm_condExpIndL1_le x

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