α : Type u_1
β : Type ?u.100460
γ : Type ?u.100463
δ : Type ?u.100466
ι : Type ?u.100469
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
f g : α → ℝ≥0∞
h : ∀ᵐ (x : α) ∂μ, f x < g x
⊢ ↑↑μ {a | ¬f a ≤ g a} = 0
α : Type u_1
β : Type ?u.100460
γ : Type ?u.100463
δ : Type ?u.100466
ι : Type ?u.100469
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
f g : α → ℝ≥0∞
h : ∀ᵐ (x : α) ∂μ, f x < g x
⊢ f ≤ᵐ[μ] g
rw [Filter.EventuallyLE, ae_iff]
α : Type u_1
β : Type ?u.100460
γ : Type ?u.100463
δ : Type ?u.100466
ι : Type ?u.100469
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
f g : α → ℝ≥0∞
h : ↑↑μ {a | ¬f a < g a} = 0
⊢ ↑↑μ {a | ¬f a ≤ g a} = 0
α : Type u_1
β : Type ?u.100460
γ : Type ?u.100463
δ : Type ?u.100466
ι : Type ?u.100469
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
f g : α → ℝ≥0∞
h : ∀ᵐ (x : α) ∂μ, f x < g x
⊢ ↑↑μ {a | ¬f a ≤ g a} = 0
rw [ae_iff] at h
α : Type u_1
β : Type ?u.100460
γ : Type ?u.100463
δ : Type ?u.100466
ι : Type ?u.100469
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
f g : α → ℝ≥0∞
h : ↑↑μ {a | ¬f a < g a} = 0
x : α
hx : x ∈ {a | ¬f a ≤ g a}
⊢ x ∈ {a | ¬f a < g a}
α : Type u_1
β : Type ?u.100460
γ : Type ?u.100463
δ : Type ?u.100466
ι : Type ?u.100469
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
f g : α → ℝ≥0∞
h : ↑↑μ {a | ¬f a < g a} = 0
⊢ ↑↑μ {a | ¬f a ≤ g a} = 0
refine' measure_mono_null (fun x hx => _) h
no goals
α : Type u_1
β : Type ?u.100460
γ : Type ?u.100463
δ : Type ?u.100466
ι : Type ?u.100469
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
f g : α → ℝ≥0∞
h : ↑↑μ {a | ¬f a < g a} = 0
x : α
hx : x ∈ {a | ¬f a ≤ g a}
⊢ x ∈ {a | ¬f a < g a}
exact not_lt.2 (le_of_lt (not_le.1 hx))