Skip to content

Commit fb290e9

Browse files
committed
fix(MeasureTheory/Integral/IntervalAverage): restore uIoc in interval average notation
1 parent 74e7346 commit fb290e9

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

Mathlib/MeasureTheory/Integral/IntervalAverage.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -44,7 +44,7 @@ variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
4444
/-- `⨍ x in a..b, f x` is the average of `f` over the interval `Ι a b` w.r.t. the Lebesgue
4545
measure. -/
4646
notation3 "⨍ "(...)" in "a".."b",
47-
"r:60:(scoped f => average (Measure.restrict volume (Ι a b)) f) => r
47+
"r:60:(scoped f => average (Measure.restrict volume (uIoc a b)) f) => r
4848

4949
theorem interval_average_symm (f : ℝ → E) (a b : ℝ) : (⨍ x in a..b, f x) = ⨍ x in b..a, f x := by
5050
rw [setAverage_eq, setAverage_eq, uIoc_comm]

0 commit comments

Comments
 (0)