α : Type u_1
β : Type u_2
E : Type ?u.2029982
F : Type ?u.2029985
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : TopologicalSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : MeasureTheory.Measure α
hf : ContinuousOn f s
hs : IsCompact s
h's : MeasurableSet s
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
⊢ AEStronglyMeasurable f (Measure.restrict μ s)
α : Type u_1
β : Type u_2
E : Type ?u.2029982
F : Type ?u.2029985
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : TopologicalSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : MeasureTheory.Measure α
hf : ContinuousOn f s
hs : IsCompact s
h's : MeasurableSet s
⊢ AEStronglyMeasurable f (Measure.restrict μ s)
letI := pseudoMetrizableSpacePseudoMetric β
α : Type u_1
β : Type u_2
E : Type ?u.2029982
F : Type ?u.2029985
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : TopologicalSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : MeasureTheory.Measure α
hf : ContinuousOn f s
hs : IsCompact s
h's : MeasurableSet s
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ AEStronglyMeasurable f (Measure.restrict μ s)
α : Type u_1
β : Type u_2
E : Type ?u.2029982
F : Type ?u.2029985
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : TopologicalSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : MeasureTheory.Measure α
hf : ContinuousOn f s
hs : IsCompact s
h's : MeasurableSet s
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
⊢ AEStronglyMeasurable f (Measure.restrict μ s)
borelize β
α : Type u_1
β : Type u_2
E : Type ?u.2029982
F : Type ?u.2029985
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : TopologicalSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : MeasureTheory.Measure α
hf : ContinuousOn f s
hs : IsCompact s
h's : MeasurableSet s
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ AEMeasurable f ∧ ∃ t, IsSeparable t ∧ ∀ᵐ (x : α) ∂Measure.restrict μ s, f x ∈ t
α : Type u_1
β : Type u_2
E : Type ?u.2029982
F : Type ?u.2029985
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : TopologicalSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : MeasureTheory.Measure α
hf : ContinuousOn f s
hs : IsCompact s
h's : MeasurableSet s
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ AEStronglyMeasurable f (Measure.restrict μ s)
rw [aestronglyMeasurable_iff_aemeasurable_separable]
case refine'_1
α : Type u_1
β : Type u_2
E : Type ?u.2029982
F : Type ?u.2029985
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : TopologicalSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : MeasureTheory.Measure α
hf : ContinuousOn f s
hs : IsCompact s
h's : MeasurableSet s
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ IsSeparable (f '' s)

case refine'_2
α : Type u_1
β : Type u_2
E : Type ?u.2029982
F : Type ?u.2029985
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : TopologicalSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : MeasureTheory.Measure α
hf : ContinuousOn f s
hs : IsCompact s
h's : MeasurableSet s
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ s, f x ∈ f '' s
α : Type u_1
β : Type u_2
E : Type ?u.2029982
F : Type ?u.2029985
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : TopologicalSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : MeasureTheory.Measure α
hf : ContinuousOn f s
hs : IsCompact s
h's : MeasurableSet s
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ AEMeasurable f ∧ ∃ t, IsSeparable t ∧ ∀ᵐ (x : α) ∂Measure.restrict μ s, f x ∈ t
refine' ⟨hf.aemeasurable h's, f '' s, _, _⟩
no goals
case refine'_1
α : Type u_1
β : Type u_2
E : Type ?u.2029982
F : Type ?u.2029985
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : TopologicalSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : MeasureTheory.Measure α
hf : ContinuousOn f s
hs : IsCompact s
h's : MeasurableSet s
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ IsSeparable (f '' s)
exact (hs.image_of_continuousOn hf).isSeparable
no goals
case refine'_2
α : Type u_1
β : Type u_2
E : Type ?u.2029982
F : Type ?u.2029985
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : TopologicalSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : MeasureTheory.Measure α
hf : ContinuousOn f s
hs : IsCompact s
h's : MeasurableSet s
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ s, f x ∈ f '' s
exact mem_of_superset (self_mem_ae_restrict h's) (subset_preimage_image _ _)