case pos
α : Type u_1
β : Type u_2
γ : Type ?u.551485
δ : Type ?u.551488
ι : Type ?u.551491
R : Type ?u.551494
R' : Type ?u.551497
m0✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
m0 : MeasurableSpace α
f : α → β
hf : MeasurableSet (range f)
μ : Measure α
h : AEMeasurable f
⊢ ∀ᵐ (x : β) ∂Measure.map f μ, x ∈ range f

case neg
α : Type u_1
β : Type u_2
γ : Type ?u.551485
δ : Type ?u.551488
ι : Type ?u.551491
R : Type ?u.551494
R' : Type ?u.551497
m0✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
m0 : MeasurableSpace α
f : α → β
hf : MeasurableSet (range f)
μ : Measure α
h : ¬AEMeasurable f
⊢ ∀ᵐ (x : β) ∂Measure.map f μ, x ∈ range f
α : Type u_1
β : Type u_2
γ : Type ?u.551485
δ : Type ?u.551488
ι : Type ?u.551491
R : Type ?u.551494
R' : Type ?u.551497
m0✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
m0 : MeasurableSpace α
f : α → β
hf : MeasurableSet (range f)
μ : Measure α
⊢ ∀ᵐ (x : β) ∂Measure.map f μ, x ∈ range f
by_cases h : AEMeasurable f μ
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.551485
δ : Type ?u.551488
ι : Type ?u.551491
R : Type ?u.551494
R' : Type ?u.551497
m0✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
m0 : MeasurableSpace α
f : α → β
hf : MeasurableSet (range f)
μ : Measure α
h : AEMeasurable f
⊢ range f ∈ ae (Measure.map f μ)
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.551485
δ : Type ?u.551488
ι : Type ?u.551491
R : Type ?u.551494
R' : Type ?u.551497
m0✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
m0 : MeasurableSpace α
f : α → β
hf : MeasurableSet (range f)
μ : Measure α
h : AEMeasurable f
⊢ ∀ᵐ (x : β) ∂Measure.map f μ, x ∈ range f
change range f ∈ (μ.map f).ae
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.551485
δ : Type ?u.551488
ι : Type ?u.551491
R : Type ?u.551494
R' : Type ?u.551497
m0✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
m0 : MeasurableSpace α
f : α → β
hf : MeasurableSet (range f)
μ : Measure α
h : AEMeasurable f
⊢ f ⁻¹' range f ∈ ae μ
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.551485
δ : Type ?u.551488
ι : Type ?u.551491
R : Type ?u.551494
R' : Type ?u.551497
m0✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
m0 : MeasurableSpace α
f : α → β
hf : MeasurableSet (range f)
μ : Measure α
h : AEMeasurable f
⊢ range f ∈ ae (Measure.map f μ)
rw [mem_ae_map_iff h hf]
case pos.hp
α : Type u_1
β : Type u_2
γ : Type ?u.551485
δ : Type ?u.551488
ι : Type ?u.551491
R : Type ?u.551494
R' : Type ?u.551497
m0✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
m0 : MeasurableSpace α
f : α → β
hf : MeasurableSet (range f)
μ : Measure α
h : AEMeasurable f
⊢ ∀ (x : α), f x ∈ range f
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.551485
δ : Type ?u.551488
ι : Type ?u.551491
R : Type ?u.551494
R' : Type ?u.551497
m0✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
m0 : MeasurableSpace α
f : α → β
hf : MeasurableSet (range f)
μ : Measure α
h : AEMeasurable f
⊢ f ⁻¹' range f ∈ ae μ
apply eventually_of_forall
no goals
case pos.hp
α : Type u_1
β : Type u_2
γ : Type ?u.551485
δ : Type ?u.551488
ι : Type ?u.551491
R : Type ?u.551494
R' : Type ?u.551497
m0✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
m0 : MeasurableSpace α
f : α → β
hf : MeasurableSet (range f)
μ : Measure α
h : AEMeasurable f
⊢ ∀ (x : α), f x ∈ range f
exact mem_range_self
no goals
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.551485
δ : Type ?u.551488
ι : Type ?u.551491
R : Type ?u.551494
R' : Type ?u.551497
m0✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
m0 : MeasurableSpace α
f : α → β
hf : MeasurableSet (range f)
μ : Measure α
h : ¬AEMeasurable f
⊢ ∀ᵐ (x : β) ∂Measure.map f μ, x ∈ range f
simp [map_of_not_aemeasurable h]