ι : Type ?u.16911495
𝕜 : Type ?u.16911498
E : Type u_1
F : Type ?u.16911504
A : Type ?u.16911507
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
a₁ a₂ a₃ : ℝ
h : a₂ ∈ Icc a₁ a₃
this : {x | x ≤ a₂} ∩ Ioc a₁ a₃ = Ioc a₁ a₂
⊢ (∫ (x : ℝ) in a₁..a₃, indicator {x | x ≤ a₂} f x ∂μ) = ∫ (x : ℝ) in a₁..a₂, f x ∂μ
ι : Type ?u.16911495
𝕜 : Type ?u.16911498
E : Type u_1
F : Type ?u.16911504
A : Type ?u.16911507
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
a₁ a₂ a₃ : ℝ
h : a₂ ∈ Icc a₁ a₃
⊢ (∫ (x : ℝ) in a₁..a₃, indicator {x | x ≤ a₂} f x ∂μ) = ∫ (x : ℝ) in a₁..a₂, f x ∂μ
have : {x | x ≤ a₂} ∩ Ioc a₁ a₃ = Ioc a₁ a₂ := Iic_inter_Ioc_of_le h.2
ι : Type ?u.16911495
𝕜 : Type ?u.16911498
E : Type u_1
F : Type ?u.16911504
A : Type ?u.16911507
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
a₁ a₂ a₃ : ℝ
h : a₂ ∈ Icc a₁ a₃
this : {x | x ≤ a₂} ∩ Ioc a₁ a₃ = Ioc a₁ a₂
⊢ MeasurableSet {x | x ≤ a₂}

ι : Type ?u.16911495
𝕜 : Type ?u.16911498
E : Type u_1
F : Type ?u.16911504
A : Type ?u.16911507
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
a₁ a₂ a₃ : ℝ
h : a₂ ∈ Icc a₁ a₃
this : {x | x ≤ a₂} ∩ Ioc a₁ a₃ = Ioc a₁ a₂
⊢ MeasurableSet {x | x ≤ a₂}
ι : Type ?u.16911495
𝕜 : Type ?u.16911498
E : Type u_1
F : Type ?u.16911504
A : Type ?u.16911507
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
a₁ a₂ a₃ : ℝ
h : a₂ ∈ Icc a₁ a₃
this : {x | x ≤ a₂} ∩ Ioc a₁ a₃ = Ioc a₁ a₂
⊢ (∫ (x : ℝ) in a₁..a₃, indicator {x | x ≤ a₂} f x ∂μ) = ∫ (x : ℝ) in a₁..a₂, f x ∂μ
rw [integral_of_le h.1, integral_of_le (h.1.trans h.2), integral_indicator,
  Measure.restrict_restrict, this]
ι : Type ?u.16911495
𝕜 : Type ?u.16911498
E : Type u_1
F : Type ?u.16911504
A : Type ?u.16911507
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
a₁ a₂ a₃ : ℝ
h : a₂ ∈ Icc a₁ a₃
this : {x | x ≤ a₂} ∩ Ioc a₁ a₃ = Ioc a₁ a₂
⊢ MeasurableSet {x | x ≤ a₂}
ι : Type ?u.16911495
𝕜 : Type ?u.16911498
E : Type u_1
F : Type ?u.16911504
A : Type ?u.16911507
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
a₁ a₂ a₃ : ℝ
h : a₂ ∈ Icc a₁ a₃
this : {x | x ≤ a₂} ∩ Ioc a₁ a₃ = Ioc a₁ a₂
⊢ MeasurableSet {x | x ≤ a₂}

ι : Type ?u.16911495
𝕜 : Type ?u.16911498
E : Type u_1
F : Type ?u.16911504
A : Type ?u.16911507
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
a₁ a₂ a₃ : ℝ
h : a₂ ∈ Icc a₁ a₃
this : {x | x ≤ a₂} ∩ Ioc a₁ a₃ = Ioc a₁ a₂
⊢ MeasurableSet {x | x ≤ a₂}
exact measurableSet_Iic
no goals
ι : Type ?u.16911495
𝕜 : Type ?u.16911498
E : Type u_1
F : Type ?u.16911504
A : Type ?u.16911507
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
a₁ a₂ a₃ : ℝ
h : a₂ ∈ Icc a₁ a₃
this : {x | x ≤ a₂} ∩ Ioc a₁ a₃ = Ioc a₁ a₂
⊢ MeasurableSet {x | x ≤ a₂}
all_goals apply measurableSet_Iic
no goals
ι : Type ?u.16911495
𝕜 : Type ?u.16911498
E : Type u_1
F : Type ?u.16911504
A : Type ?u.16911507
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
a₁ a₂ a₃ : ℝ
h : a₂ ∈ Icc a₁ a₃
this : {x | x ≤ a₂} ∩ Ioc a₁ a₃ = Ioc a₁ a₂
⊢ MeasurableSet {x | x ≤ a₂}
apply measurableSet_Iic