α : Type u_1
β : Type ?u.984332
γ : Type ?u.984335
δ : Type ?u.984338
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hg : AEMeasurable g
hfi : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
h_le : f ≤ᵐ[μ] g
h : (∫⁻ (x : α), g x ∂μ) ≤ ∫⁻ (x : α), f x ∂μ
⊢ ¬∃ᵐ (x : α) ∂μ, f x ≠ g x
α : Type u_1
β : Type ?u.984332
γ : Type ?u.984335
δ : Type ?u.984338
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hg : AEMeasurable g
hfi : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
h_le : f ≤ᵐ[μ] g
h : ∃ᵐ (x : α) ∂μ, f x ≠ g x
⊢ (∫⁻ (x : α), f x ∂μ) < ∫⁻ (x : α), g x ∂μ
contrapose! h
α : Type u_1
β : Type ?u.984332
γ : Type ?u.984335
δ : Type ?u.984338
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hg : AEMeasurable g
hfi : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
h_le : f ≤ᵐ[μ] g
h : (∫⁻ (x : α), g x ∂μ) ≤ ∫⁻ (x : α), f x ∂μ
⊢ ∀ᵐ (x : α) ∂μ, f x = g x
α : Type u_1
β : Type ?u.984332
γ : Type ?u.984335
δ : Type ?u.984338
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hg : AEMeasurable g
hfi : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
h_le : f ≤ᵐ[μ] g
h : (∫⁻ (x : α), g x ∂μ) ≤ ∫⁻ (x : α), f x ∂μ
⊢ ¬∃ᵐ (x : α) ∂μ, f x ≠ g x
simp only [not_frequently, Ne.def, Classical.not_not]
no goals
α : Type u_1
β : Type ?u.984332
γ : Type ?u.984335
δ : Type ?u.984338
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hg : AEMeasurable g
hfi : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
h_le : f ≤ᵐ[μ] g
h : (∫⁻ (x : α), g x ∂μ) ≤ ∫⁻ (x : α), f x ∂μ
⊢ ∀ᵐ (x : α) ∂μ, f x = g x
exact ae_eq_of_ae_le_of_lintegral_le h_le hfi hg h