We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent f6d15e2 commit d98c33eCopy full SHA for d98c33e
1 file changed
Mathlib/MeasureTheory/Integral/IntervalAverage.lean
@@ -44,7 +44,7 @@ variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
44
/-- `⨍ x in a..b, f x` is the average of `f` over the interval `Ι a b` w.r.t. the Lebesgue
45
measure. -/
46
notation3 "⨍ "(...)" in "a".."b",
47
- "r:60:(scoped f => average (Measure.restrict volume (Ι a b)) f) => r
+ "r:60:(scoped f => average (Measure.restrict volume (uIoc a b)) f) => r
48
49
theorem interval_average_symm (f : ℝ → E) (a b : ℝ) : (⨍ x in a..b, f x) = ⨍ x in b..a, f x := by
50
rw [setAverage_eq, setAverage_eq, uIoc_comm]
0 commit comments