Skip to content

Commit 54b0ef5

Browse files
committed
chore(MeasureTheory/Integral/Lebesgue/Map): remove an erw (#38502)
- rewrites `lintegral_indicator_const_comp` to replace `erw [lintegral_comp ...]` with a plain `rw` - uses `lintegral_map` at the start of the rewrite chain before `lintegral_indicator_const` and `Measure.map_apply` Extracted from #38415 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)
1 parent 0006bd5 commit 54b0ef5

1 file changed

Lines changed: 2 additions & 2 deletions

File tree

  • Mathlib/MeasureTheory/Integral/Lebesgue

Mathlib/MeasureTheory/Integral/Lebesgue/Map.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -72,8 +72,8 @@ theorem setLIntegral_map {f : β → ℝ≥0∞} {g : α → β} {s : Set β}
7272
theorem lintegral_indicator_const_comp {f : α → β} {s : Set β}
7373
(hf : Measurable f) (hs : MeasurableSet s) (c : ℝ≥0∞) :
7474
∫⁻ a, s.indicator (fun _ => c) (f a) ∂μ = c * μ (f ⁻¹' s) := by
75-
erw [lintegral_comp (measurable_const.indicator hs) hf]
76-
rw [lintegral_indicator_const hs, Measure.map_apply hf hs]
75+
rw [← lintegral_map (measurable_const.indicator hs) hf, lintegral_indicator_const hs,
76+
Measure.map_apply hf hs]
7777

7878
/-- If `g : α → β` is a measurable embedding and `f : β → ℝ≥0∞` is any function (not necessarily
7979
measurable), then `∫⁻ a, f a ∂(map g μ) = ∫⁻ a, f (g a) ∂μ`. Compare with `lintegral_map` which

0 commit comments

Comments
 (0)