α : Type u_1
β : Type u_2
γ : Type ?u.348372
ι : Type ?u.348375
inst✝² : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f g : α → β
hf : AEStronglyMeasurable f μ
⊢ ∀ᵐ (x : α) ∂μ, f x ∈ range (AEStronglyMeasurable.mk f hf)
α : Type u_1
β : Type u_2
γ : Type ?u.348372
ι : Type ?u.348375
inst✝² : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f g : α → β
hf : AEStronglyMeasurable f μ
⊢ ∃ t, IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, f x ∈ t
refine' ⟨range (hf.mk f), hf.stronglyMeasurable_mk.isSeparable_range, _⟩
case h
α : Type u_1
β : Type u_2
γ : Type ?u.348372
ι : Type ?u.348375
inst✝² : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f g : α → β
hf : AEStronglyMeasurable f μ
x : α
hx : f x = AEStronglyMeasurable.mk f hf x
⊢ f x ∈ range (AEStronglyMeasurable.mk f hf)
α : Type u_1
β : Type u_2
γ : Type ?u.348372
ι : Type ?u.348375
inst✝² : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f g : α → β
hf : AEStronglyMeasurable f μ
⊢ ∀ᵐ (x : α) ∂μ, f x ∈ range (AEStronglyMeasurable.mk f hf)
filter_upwards [hf.ae_eq_mk] with x hx
no goals
case h
α : Type u_1
β : Type u_2
γ : Type ?u.348372
ι : Type ?u.348375
inst✝² : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f g : α → β
hf : AEStronglyMeasurable f μ
x : α
hx : f x = AEStronglyMeasurable.mk f hf x
⊢ f x ∈ range (AEStronglyMeasurable.mk f hf)
simp [hx]