volume — Mathlib

English

BoxAdditiveMap.volume assigns to each box the continuous linear endomorphism x ↦ (volume J).toReal · x.

Русский

BoxAdditiveMap.volume отображает для каждой коробки линейное преобразование x ↦ (volume J).toReal · x.

LaTeX

$$$BoxAdditiveMap.volume(J) : E \\to_L[\\mathbb{R}] E \\,=\\, \\text{(volume J).toReal} \\cdot \\mathrm{id}_E$$$

Lean4

/-- Box-additive map sending each box `I` to the continuous linear endomorphism
`x ↦ (volume I).toReal • x`. -/
protected def volume {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] : ι →ᵇᵃ E →L[ℝ] E :=
  (volume : Measure (ι → ℝ)).toBoxAdditive.toSMul

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