α : Type ?u.877436
β : Type u_1
γ : Type u_2
γ₂ : Type ?u.877445
δ : Type ?u.877448
ι : Sort y
s t u : Set α
inst✝¹⁵ : TopologicalSpace α
inst✝¹⁴ : MeasurableSpace α
inst✝¹³ : OpensMeasurableSpace α
inst✝¹² : TopologicalSpace β
inst✝¹¹ : MeasurableSpace β
inst✝¹⁰ : OpensMeasurableSpace β
inst✝⁹ : TopologicalSpace γ
inst✝⁸ : MeasurableSpace γ
inst✝⁷ : BorelSpace γ
inst✝⁶ : TopologicalSpace γ₂
inst✝⁵ : MeasurableSpace γ₂
inst✝⁴ : BorelSpace γ₂
inst✝³ : MeasurableSpace δ
α' : Type ?u.877541
inst✝² : TopologicalSpace α'
inst✝¹ : MeasurableSpace α'
f : β → γ
hf : Continuous f
hf_surj : Function.Surjective f
μ : MeasureTheory.Measure β
inst✝ : Measure.IsOpenPosMeasure μ
U : Set γ
hUo : IsOpen U
hUne : Set.Nonempty U
⊢ ↑↑(Measure.map f μ) U ≠ 0
α : Type ?u.877436
β : Type u_1
γ : Type u_2
γ₂ : Type ?u.877445
δ : Type ?u.877448
ι : Sort y
s t u : Set α
inst✝¹⁵ : TopologicalSpace α
inst✝¹⁴ : MeasurableSpace α
inst✝¹³ : OpensMeasurableSpace α
inst✝¹² : TopologicalSpace β
inst✝¹¹ : MeasurableSpace β
inst✝¹⁰ : OpensMeasurableSpace β
inst✝⁹ : TopologicalSpace γ
inst✝⁸ : MeasurableSpace γ
inst✝⁷ : BorelSpace γ
inst✝⁶ : TopologicalSpace γ₂
inst✝⁵ : MeasurableSpace γ₂
inst✝⁴ : BorelSpace γ₂
inst✝³ : MeasurableSpace δ
α' : Type ?u.877541
inst✝² : TopologicalSpace α'
inst✝¹ : MeasurableSpace α'
f : β → γ
hf : Continuous f
hf_surj : Function.Surjective f
μ : MeasureTheory.Measure β
inst✝ : Measure.IsOpenPosMeasure μ
⊢ Measure.IsOpenPosMeasure (Measure.map f μ)
refine' ⟨fun U hUo hUne => _⟩
α : Type ?u.877436
β : Type u_1
γ : Type u_2
γ₂ : Type ?u.877445
δ : Type ?u.877448
ι : Sort y
s t u : Set α
inst✝¹⁵ : TopologicalSpace α
inst✝¹⁴ : MeasurableSpace α
inst✝¹³ : OpensMeasurableSpace α
inst✝¹² : TopologicalSpace β
inst✝¹¹ : MeasurableSpace β
inst✝¹⁰ : OpensMeasurableSpace β
inst✝⁹ : TopologicalSpace γ
inst✝⁸ : MeasurableSpace γ
inst✝⁷ : BorelSpace γ
inst✝⁶ : TopologicalSpace γ₂
inst✝⁵ : MeasurableSpace γ₂
inst✝⁴ : BorelSpace γ₂
inst✝³ : MeasurableSpace δ
α' : Type ?u.877541
inst✝² : TopologicalSpace α'
inst✝¹ : MeasurableSpace α'
f : β → γ
hf : Continuous f
hf_surj : Function.Surjective f
μ : MeasureTheory.Measure β
inst✝ : Measure.IsOpenPosMeasure μ
U : Set γ
hUo : IsOpen U
hUne : Set.Nonempty U
⊢ ↑↑μ (f ⁻¹' U) ≠ 0
α : Type ?u.877436
β : Type u_1
γ : Type u_2
γ₂ : Type ?u.877445
δ : Type ?u.877448
ι : Sort y
s t u : Set α
inst✝¹⁵ : TopologicalSpace α
inst✝¹⁴ : MeasurableSpace α
inst✝¹³ : OpensMeasurableSpace α
inst✝¹² : TopologicalSpace β
inst✝¹¹ : MeasurableSpace β
inst✝¹⁰ : OpensMeasurableSpace β
inst✝⁹ : TopologicalSpace γ
inst✝⁸ : MeasurableSpace γ
inst✝⁷ : BorelSpace γ
inst✝⁶ : TopologicalSpace γ₂
inst✝⁵ : MeasurableSpace γ₂
inst✝⁴ : BorelSpace γ₂
inst✝³ : MeasurableSpace δ
α' : Type ?u.877541
inst✝² : TopologicalSpace α'
inst✝¹ : MeasurableSpace α'
f : β → γ
hf : Continuous f
hf_surj : Function.Surjective f
μ : MeasureTheory.Measure β
inst✝ : Measure.IsOpenPosMeasure μ
U : Set γ
hUo : IsOpen U
hUne : Set.Nonempty U
⊢ ↑↑(Measure.map f μ) U ≠ 0
rw [Measure.map_apply hf.measurable hUo.measurableSet]
no goals
α : Type ?u.877436
β : Type u_1
γ : Type u_2
γ₂ : Type ?u.877445
δ : Type ?u.877448
ι : Sort y
s t u : Set α
inst✝¹⁵ : TopologicalSpace α
inst✝¹⁴ : MeasurableSpace α
inst✝¹³ : OpensMeasurableSpace α
inst✝¹² : TopologicalSpace β
inst✝¹¹ : MeasurableSpace β
inst✝¹⁰ : OpensMeasurableSpace β
inst✝⁹ : TopologicalSpace γ
inst✝⁸ : MeasurableSpace γ
inst✝⁷ : BorelSpace γ
inst✝⁶ : TopologicalSpace γ₂
inst✝⁵ : MeasurableSpace γ₂
inst✝⁴ : BorelSpace γ₂
inst✝³ : MeasurableSpace δ
α' : Type ?u.877541
inst✝² : TopologicalSpace α'
inst✝¹ : MeasurableSpace α'
f : β → γ
hf : Continuous f
hf_surj : Function.Surjective f
μ : MeasureTheory.Measure β
inst✝ : Measure.IsOpenPosMeasure μ
U : Set γ
hUo : IsOpen U
hUne : Set.Nonempty U
⊢ ↑↑μ (f ⁻¹' U) ≠ 0
exact (hUo.preimage hf).measure_ne_zero μ (hf_surj.nonempty_preimage.mpr hUne)