α : Type u_1
β : Type u_2
γ : Type ?u.4867261
δ : Type ?u.4867264
ι : Type ?u.4867267
R : Type ?u.4867270
R' : Type ?u.4867273
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
s t : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = OfNat.ofNat 0 x
⊢ indicator s f =ᶠ[ae μ] 0
α : Type u_1
β : Type u_2
γ : Type ?u.4867261
δ : Type ?u.4867264
ι : Type ?u.4867267
R : Type ?u.4867270
R' : Type ?u.4867273
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
s t : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
hf : f =ᶠ[ae (Measure.restrict μ s)] 0
⊢ indicator s f =ᶠ[ae μ] 0
rw [Filter.EventuallyEq, ae_restrict_iff' hs] at hf
case h
α : Type u_1
β : Type u_2
γ : Type ?u.4867261
δ : Type ?u.4867264
ι : Type ?u.4867267
R : Type ?u.4867270
R' : Type ?u.4867273
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
s t : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = OfNat.ofNat 0 x
x : α
hx : x ∈ s → f x = OfNat.ofNat 0 x
⊢ indicator s f x = OfNat.ofNat 0 x
α : Type u_1
β : Type u_2
γ : Type ?u.4867261
δ : Type ?u.4867264
ι : Type ?u.4867267
R : Type ?u.4867270
R' : Type ?u.4867273
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
s t : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = OfNat.ofNat 0 x
⊢ indicator s f =ᶠ[ae μ] 0
filter_upwards [hf]with x hx
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.4867261
δ : Type ?u.4867264
ι : Type ?u.4867267
R : Type ?u.4867270
R' : Type ?u.4867273
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
s t : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = OfNat.ofNat 0 x
x : α
hx : x ∈ s → f x = OfNat.ofNat 0 x
hxs : x ∈ s
⊢ indicator s f x = OfNat.ofNat 0 x

case neg
α : Type u_1
β : Type u_2
γ : Type ?u.4867261
δ : Type ?u.4867264
ι : Type ?u.4867267
R : Type ?u.4867270
R' : Type ?u.4867273
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
s t : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = OfNat.ofNat 0 x
x : α
hx : x ∈ s → f x = OfNat.ofNat 0 x
hxs : ¬x ∈ s
⊢ indicator s f x = OfNat.ofNat 0 x
case h
α : Type u_1
β : Type u_2
γ : Type ?u.4867261
δ : Type ?u.4867264
ι : Type ?u.4867267
R : Type ?u.4867270
R' : Type ?u.4867273
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
s t : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = OfNat.ofNat 0 x
x : α
hx : x ∈ s → f x = OfNat.ofNat 0 x
⊢ indicator s f x = OfNat.ofNat 0 x
by_cases hxs : x ∈ s
no goals
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.4867261
δ : Type ?u.4867264
ι : Type ?u.4867267
R : Type ?u.4867270
R' : Type ?u.4867273
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
s t : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = OfNat.ofNat 0 x
x : α
hx : x ∈ s → f x = OfNat.ofNat 0 x
hxs : x ∈ s
⊢ indicator s f x = OfNat.ofNat 0 x
simp only [hxs, hx hxs, Set.indicator_of_mem]
no goals
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.4867261
δ : Type ?u.4867264
ι : Type ?u.4867267
R : Type ?u.4867270
R' : Type ?u.4867273
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
s t : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = OfNat.ofNat 0 x
x : α
hx : x ∈ s → f x = OfNat.ofNat 0 x
hxs : ¬x ∈ s
⊢ indicator s f x = OfNat.ofNat 0 x
simp [hx, hxs]