α : Type u_1
β : Type u_2
γ : Type ?u.5024740
δ : Type ?u.5024743
ι : Type ?u.5024746
R : Type ?u.5024749
R' : Type ?u.5024752
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
s t : Set α
f : α → β
inst✝ : Zero β
g : α → β
hs : MeasurableSet s
⊢ (∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x) ↔ indicator s f =ᶠ[ae μ] indicator s g
α : Type u_1
β : Type u_2
γ : Type ?u.5024740
δ : Type ?u.5024743
ι : Type ?u.5024746
R : Type ?u.5024749
R' : Type ?u.5024752
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
s t : Set α
f : α → β
inst✝ : Zero β
g : α → β
hs : MeasurableSet s
⊢ f =ᶠ[ae (Measure.restrict μ s)] g ↔ indicator s f =ᶠ[ae μ] indicator s g
rw [Filter.EventuallyEq, ae_restrict_iff' hs]
case h
α : Type u_1
β : Type u_2
γ : Type ?u.5024740
δ : Type ?u.5024743
ι : Type ?u.5024746
R : Type ?u.5024749
R' : Type ?u.5024752
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
s t : Set α
f : α → β
inst✝ : Zero β
g : α → β
hs : MeasurableSet s
h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
x : α
hx : x ∈ s → f x = g x
⊢ indicator s f x = indicator s g x

case h
α : Type u_1
β : Type u_2
γ : Type ?u.5024740
δ : Type ?u.5024743
ι : Type ?u.5024746
R : Type ?u.5024749
R' : Type ?u.5024752
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
s t : Set α
f : α → β
inst✝ : Zero β
g : α → β
hs : MeasurableSet s
h : indicator s f =ᶠ[ae μ] indicator s g
x : α
hx : indicator s f x = indicator s g x
⊢ x ∈ s → f x = g x
α : Type u_1
β : Type u_2
γ : Type ?u.5024740
δ : Type ?u.5024743
ι : Type ?u.5024746
R : Type ?u.5024749
R' : Type ?u.5024752
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
s t : Set α
f : α → β
inst✝ : Zero β
g : α → β
hs : MeasurableSet s
⊢ (∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x) ↔ indicator s f =ᶠ[ae μ] indicator s g
refine' ⟨fun h => _, fun h => _⟩ <;> filter_upwards [h]with x hx
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.5024740
δ : Type ?u.5024743
ι : Type ?u.5024746
R : Type ?u.5024749
R' : Type ?u.5024752
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
s t : Set α
f : α → β
inst✝ : Zero β
g : α → β
hs : MeasurableSet s
h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
x : α
hx : x ∈ s → f x = g x
hxs : x ∈ s
⊢ indicator s f x = indicator s g x

case neg
α : Type u_1
β : Type u_2
γ : Type ?u.5024740
δ : Type ?u.5024743
ι : Type ?u.5024746
R : Type ?u.5024749
R' : Type ?u.5024752
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
s t : Set α
f : α → β
inst✝ : Zero β
g : α → β
hs : MeasurableSet s
h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
x : α
hx : x ∈ s → f x = g x
hxs : ¬x ∈ s
⊢ indicator s f x = indicator s g x
case h
α : Type u_1
β : Type u_2
γ : Type ?u.5024740
δ : Type ?u.5024743
ι : Type ?u.5024746
R : Type ?u.5024749
R' : Type ?u.5024752
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
s t : Set α
f : α → β
inst✝ : Zero β
g : α → β
hs : MeasurableSet s
h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
x : α
hx : x ∈ s → f x = g x
⊢ indicator s f x = indicator s g x
by_cases hxs : x ∈ s
no goals
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.5024740
δ : Type ?u.5024743
ι : Type ?u.5024746
R : Type ?u.5024749
R' : Type ?u.5024752
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
s t : Set α
f : α → β
inst✝ : Zero β
g : α → β
hs : MeasurableSet s
h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
x : α
hx : x ∈ s → f x = g x
hxs : x ∈ s
⊢ indicator s f x = indicator s g x
simp [hxs, hx hxs]
no goals
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.5024740
δ : Type ?u.5024743
ι : Type ?u.5024746
R : Type ?u.5024749
R' : Type ?u.5024752
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
s t : Set α
f : α → β
inst✝ : Zero β
g : α → β
hs : MeasurableSet s
h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
x : α
hx : x ∈ s → f x = g x
hxs : ¬x ∈ s
⊢ indicator s f x = indicator s g x
simp [hxs]
case h
α : Type u_1
β : Type u_2
γ : Type ?u.5024740
δ : Type ?u.5024743
ι : Type ?u.5024746
R : Type ?u.5024749
R' : Type ?u.5024752
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
s t : Set α
f : α → β
inst✝ : Zero β
g : α → β
hs : MeasurableSet s
h : indicator s f =ᶠ[ae μ] indicator s g
x : α
hx : indicator s f x = indicator s g x
hxs : x ∈ s
⊢ f x = g x
case h
α : Type u_1
β : Type u_2
γ : Type ?u.5024740
δ : Type ?u.5024743
ι : Type ?u.5024746
R : Type ?u.5024749
R' : Type ?u.5024752
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
s t : Set α
f : α → β
inst✝ : Zero β
g : α → β
hs : MeasurableSet s
h : indicator s f =ᶠ[ae μ] indicator s g
x : α
hx : indicator s f x = indicator s g x
⊢ x ∈ s → f x = g x
intro hxs
no goals
case h
α : Type u_1
β : Type u_2
γ : Type ?u.5024740
δ : Type ?u.5024743
ι : Type ?u.5024746
R : Type ?u.5024749
R' : Type ?u.5024752
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
s t : Set α
f : α → β
inst✝ : Zero β
g : α → β
hs : MeasurableSet s
h : indicator s f =ᶠ[ae μ] indicator s g
x : α
hx : indicator s f x = indicator s g x
hxs : x ∈ s
⊢ f x = g x
simpa [hxs] using hx