Skip to content

Commit 8be6a9b

Browse files
committed
Update L1.lean
1 parent f7d0ddf commit 8be6a9b

1 file changed

Lines changed: 2 additions & 0 deletions

File tree

  • Mathlib/MeasureTheory/VectorMeasure/Integral

Mathlib/MeasureTheory/VectorMeasure/Integral/L1.lean

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -189,6 +189,8 @@ variable {α E F G : Type*} [MeasurableSpace α]
189189
[NormedAddCommGroup G] [NormedSpace ℝ G]
190190
(Bμ : VectorMeasureWithPairing α E F G)
191191

192+
/-- Given `Bμ : VectorMeasureWithPairing` and a set `s`. `Bμ.restrict s` only restrict
193+
the vector measure to `s` without changing the pairing. -/
192194
noncomputable def restrict (s : Set α) : VectorMeasureWithPairing α E F G :=
193195
VectorMeasureWithPairing.mk Bμ.pairing (Bμ.vectorMeasure.restrict s)
194196

0 commit comments

Comments
 (0)