add_compLpL — Mathlib

English

The operator of composing with a sum of two maps distributes over the sum of their induced Lp-operators.

Русский

Операция композиции с суммой отображений распределяется по сумме соответствующих операций на Lp.

LaTeX

$$$ (L+L').compLpL\\, p\\, μ = L.compLpL\\, p\\, μ + L'.compLpL\\, p\\, μ.$$$

Lean4

theorem add_compLpL [Fact (1 ≤ p)] (L L' : E →SL[σ] F) : (L + L').compLpL p μ = L.compLpL p μ + L'.compLpL p μ := by
  ext1 f; exact add_compLp L L' f

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