Skip to content

Commit 9baa9e8

Browse files
committed
doc(MeasureTheory): remove stale paragraph (leanprover-community#33278)
- Remove a paragraph describing definition of notation that does not happen in this file. - Also align a scalar multiplication symbol in the docs with the symbol used in the code.
1 parent b8e3880 commit 9baa9e8

1 file changed

Lines changed: 1 addition & 4 deletions

File tree

  • Mathlib/MeasureTheory/Integral/Bochner

Mathlib/MeasureTheory/Integral/Bochner/L1.lean

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@ and corresponding API.
2121
The Bochner integral is defined through the extension process described in the file
2222
`Mathlib/MeasureTheory/Integral/SetToL1.lean`, which follows these steps:
2323
24-
1. Define the integral of the indicator of a set. This is `weightedSMul μ s x = μ.real s * x`.
24+
1. Define the integral of the indicator of a set. This is `weightedSMul μ s x = μ.real s x`.
2525
`weightedSMul μ` is shown to be linear in the value `x` and `DominatedFinMeasAdditive`
2626
(defined in the file `Mathlib/MeasureTheory/Integral/SetToL1.lean`) with respect to the set `s`.
2727
@@ -44,9 +44,6 @@ The Bochner integral is defined through the extension process described in the f
4444
* `α →₁ₛ[μ] E` : simple functions in L1 space, i.e., equivalence classes of integrable simple
4545
functions (defined in `Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean`)
4646
47-
We also define notations for integral on a set, which are described in the file
48-
`Mathlib/MeasureTheory/Integral/SetIntegral.lean`.
49-
5047
Note: `ₛ` is typed using `\_s`. Sometimes it shows as a box if the font is missing.
5148
5249
## Tags

0 commit comments

Comments
 (0)