α : Type u_1
β : Type ?u.1776303
γ : Type ?u.1776306
δ : Type ?u.1776309
m : MeasurableSpace α
μ ν : Measure α
p : α → Prop
f : α → ℝ≥0∞
hf : Measurable f
⊢ (↑↑μ ({x | f x ≠ 0} ∩ {a | ¬p a}) = 0) = (↑↑μ {a | ¬(f a ≠ 0 → p a)} = 0)
α : Type u_1
β : Type ?u.1776303
γ : Type ?u.1776306
δ : Type ?u.1776309
m : MeasurableSpace α
μ ν : Measure α
p : α → Prop
f : α → ℝ≥0∞
hf : Measurable f
⊢ (∀ᵐ (x : α) ∂withDensity μ f, p x) ↔ ∀ᵐ (x : α) ∂μ, f x ≠ 0 → p x
rw [ae_iff, ae_iff, withDensity_apply_eq_zero hf, iff_iff_eq]
case e_a.e_a
α : Type u_1
β : Type ?u.1776303
γ : Type ?u.1776306
δ : Type ?u.1776309
m : MeasurableSpace α
μ ν : Measure α
p : α → Prop
f : α → ℝ≥0∞
hf : Measurable f
⊢ {x | f x ≠ 0} ∩ {a | ¬p a} = {a | ¬(f a ≠ 0 → p a)}
α : Type u_1
β : Type ?u.1776303
γ : Type ?u.1776306
δ : Type ?u.1776309
m : MeasurableSpace α
μ ν : Measure α
p : α → Prop
f : α → ℝ≥0∞
hf : Measurable f
⊢ (↑↑μ ({x | f x ≠ 0} ∩ {a | ¬p a}) = 0) = (↑↑μ {a | ¬(f a ≠ 0 → p a)} = 0)
congr
case e_a.e_a.h
α : Type u_1
β : Type ?u.1776303
γ : Type ?u.1776306
δ : Type ?u.1776309
m : MeasurableSpace α
μ ν : Measure α
p : α → Prop
f : α → ℝ≥0∞
hf : Measurable f
x : α
⊢ x ∈ {x | f x ≠ 0} ∩ {a | ¬p a} ↔ x ∈ {a | ¬(f a ≠ 0 → p a)}
case e_a.e_a
α : Type u_1
β : Type ?u.1776303
γ : Type ?u.1776306
δ : Type ?u.1776309
m : MeasurableSpace α
μ ν : Measure α
p : α → Prop
f : α → ℝ≥0∞
hf : Measurable f
⊢ {x | f x ≠ 0} ∩ {a | ¬p a} = {a | ¬(f a ≠ 0 → p a)}
ext x
no goals
case e_a.e_a.h
α : Type u_1
β : Type ?u.1776303
γ : Type ?u.1776306
δ : Type ?u.1776309
m : MeasurableSpace α
μ ν : Measure α
p : α → Prop
f : α → ℝ≥0∞
hf : Measurable f
x : α
⊢ x ∈ {x | f x ≠ 0} ∩ {a | ¬p a} ↔ x ∈ {a | ¬(f a ≠ 0 → p a)}
simp only [exists_prop, mem_inter_iff, iff_self_iff, mem_setOf_eq, not_forall]