α : Type u_1
β : Type ?u.294994
γ : Type ?u.294997
δ : Type ?u.295000
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
⊢ (fun x => f x) =ᵐ[Measure.restrict μ s] fun a => g a
α : Type u_1
β : Type ?u.294994
γ : Type ?u.294997
δ : Type ?u.295000
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
⊢ (∫⁻ (x : α) in s, f x ∂μ) = ∫⁻ (x : α) in s, g x ∂μ
rw [lintegral_congr_ae]
α : Type u_1
β : Type ?u.294994
γ : Type ?u.294997
δ : Type ?u.295000
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ s, f x = g x
α : Type u_1
β : Type ?u.294994
γ : Type ?u.294997
δ : Type ?u.295000
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
⊢ (fun x => f x) =ᵐ[Measure.restrict μ s] fun a => g a
rw [EventuallyEq]
no goals
α : Type u_1
β : Type ?u.294994
γ : Type ?u.294997
δ : Type ?u.295000
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ s, f x = g x
rwa [ae_restrict_iff' hs]