α : Type u_1
β : Type u_2
γ : Type ?u.4814398
δ : Type ?u.4814401
ι : Type ?u.4814404
R : Type ?u.4814407
R' : Type ?u.4814410
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 μ] f
α : Type u_1
β : Type u_2
γ : Type ?u.4814398
δ : Type ?u.4814401
ι : Type ?u.4814404
R : Type ?u.4814407
R' : Type ?u.4814410
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
s t : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
hf : f =ᶠ[ae (Measure.restrict μ (sᶜ))] 0
⊢ indicator s f =ᶠ[ae μ] f
rw [Filter.EventuallyEq, ae_restrict_iff' hs.compl] at hf
case h
α : Type u_1
β : Type u_2
γ : Type ?u.4814398
δ : Type ?u.4814401
ι : Type ?u.4814404
R : Type ?u.4814407
R' : Type ?u.4814410
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 = f x
α : Type u_1
β : Type u_2
γ : Type ?u.4814398
δ : Type ?u.4814401
ι : Type ?u.4814404
R : Type ?u.4814407
R' : Type ?u.4814410
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 μ] f
filter_upwards [hf]with x hx
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.4814398
δ : Type ?u.4814401
ι : Type ?u.4814404
R : Type ?u.4814407
R' : Type ?u.4814410
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 = f x

case neg
α : Type u_1
β : Type u_2
γ : Type ?u.4814398
δ : Type ?u.4814401
ι : Type ?u.4814404
R : Type ?u.4814407
R' : Type ?u.4814410
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 = f x
case h
α : Type u_1
β : Type u_2
γ : Type ?u.4814398
δ : Type ?u.4814401
ι : Type ?u.4814404
R : Type ?u.4814407
R' : Type ?u.4814410
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 = f x
by_cases hxs : x ∈ s
no goals
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.4814398
δ : Type ?u.4814401
ι : Type ?u.4814404
R : Type ?u.4814407
R' : Type ?u.4814410
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 = f x
simp only [hxs, Set.indicator_of_mem]
no goals
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.4814398
δ : Type ?u.4814401
ι : Type ?u.4814404
R : Type ?u.4814407
R' : Type ?u.4814410
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 = f x
simp only [hx hxs, Pi.zero_apply, Set.indicator_apply_eq_zero, eq_self_iff_true, imp_true_iff]