α : Type u_1
β : Type ?u.1777451
γ : Type ?u.1777454
δ : Type ?u.1777457
m : MeasurableSpace α
μ ν : Measure α
p : α → Prop
f : α → ℝ≥0∞
hf : Measurable f
⊢ (∀ᵐ (x : α) ∂μ, f x ≠ 0 → p x) ↔ ∀ᵐ (x : α) ∂μ, x ∈ {x | f x ≠ 0} → p x

α : Type u_1
β : Type ?u.1777451
γ : Type ?u.1777454
δ : Type ?u.1777457
m : MeasurableSpace α
μ ν : Measure α
p : α → Prop
f : α → ℝ≥0∞
hf : Measurable f
⊢ MeasurableSet {x | f x ≠ 0}
α : Type u_1
β : Type ?u.1777451
γ : Type ?u.1777454
δ : Type ?u.1777457
m : MeasurableSpace α
μ ν : Measure α
p : α → Prop
f : α → ℝ≥0∞
hf : Measurable f
⊢ (∀ᵐ (x : α) ∂withDensity μ f, p x) ↔ ∀ᵐ (x : α) ∂Measure.restrict μ {x | f x ≠ 0}, p x
rw [ae_withDensity_iff hf, ae_restrict_iff']
no goals
α : Type u_1
β : Type ?u.1777451
γ : Type ?u.1777454
δ : Type ?u.1777457
m : MeasurableSpace α
μ ν : Measure α
p : α → Prop
f : α → ℝ≥0∞
hf : Measurable f
⊢ (∀ᵐ (x : α) ∂μ, f x ≠ 0 → p x) ↔ ∀ᵐ (x : α) ∂μ, x ∈ {x | f x ≠ 0} → p x
rfl
no goals
α : Type u_1
β : Type ?u.1777451
γ : Type ?u.1777454
δ : Type ?u.1777457
m : MeasurableSpace α
μ ν : Measure α
p : α → Prop
f : α → ℝ≥0∞
hf : Measurable f
⊢ MeasurableSet {x | f x ≠ 0}
exact hf (measurableSet_singleton 0).compl