α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace α
μ✝ : Measure α
inst✝⁴ : OpensMeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : BorelSpace β
f : α ≃ₜ β
μ : Measure α
inst✝ : OuterRegular μ
A : Set β
hA : MeasurableSet A
r : ℝ≥0∞
hr : r > ↑↑(map (↑f) μ) A
⊢ ∃ U, U ⊇ A ∧ IsOpen U ∧ ↑↑(map (↑f) μ) U < r
α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace α
μ✝ : Measure α
inst✝⁴ : OpensMeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : BorelSpace β
f : α ≃ₜ β
μ : Measure α
inst✝ : OuterRegular μ
⊢ OuterRegular (map (↑f) μ)
refine' ⟨fun A hA r hr => _⟩
α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace α
μ✝ : Measure α
inst✝⁴ : OpensMeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : BorelSpace β
f : α ≃ₜ β
μ : Measure α
inst✝ : OuterRegular μ
A : Set β
hA : MeasurableSet A
r : ℝ≥0∞
hr : r > ↑↑μ (↑(Homeomorph.symm f) '' A)
⊢ ∃ U, U ⊇ A ∧ IsOpen U ∧ ↑↑(map (↑f) μ) U < r
α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace α
μ✝ : Measure α
inst✝⁴ : OpensMeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : BorelSpace β
f : α ≃ₜ β
μ : Measure α
inst✝ : OuterRegular μ
A : Set β
hA : MeasurableSet A
r : ℝ≥0∞
hr : r > ↑↑(map (↑f) μ) A
⊢ ∃ U, U ⊇ A ∧ IsOpen U ∧ ↑↑(map (↑f) μ) U < r
rw [map_apply f.measurable hA, ← f.image_symm] at hr
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace α
μ✝ : Measure α
inst✝⁴ : OpensMeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : BorelSpace β
f : α ≃ₜ β
μ : Measure α
inst✝ : OuterRegular μ
A : Set β
hA : MeasurableSet A
r : ℝ≥0∞
hr : r > ↑↑μ (↑(Homeomorph.symm f) '' A)
U : Set α
hAU : U ⊇ ↑(Homeomorph.symm f) '' A
hUo : IsOpen U
hU : ↑↑μ U < r
⊢ ∃ U, U ⊇ A ∧ IsOpen U ∧ ↑↑(map (↑f) μ) U < r
α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace α
μ✝ : Measure α
inst✝⁴ : OpensMeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : BorelSpace β
f : α ≃ₜ β
μ : Measure α
inst✝ : OuterRegular μ
A : Set β
hA : MeasurableSet A
r : ℝ≥0∞
hr : r > ↑↑μ (↑(Homeomorph.symm f) '' A)
⊢ ∃ U, U ⊇ A ∧ IsOpen U ∧ ↑↑(map (↑f) μ) U < r
rcases Set.exists_isOpen_lt_of_lt _ r hr with ⟨U, hAU, hUo, hU⟩
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace α
μ✝ : Measure α
inst✝⁴ : OpensMeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : BorelSpace β
f : α ≃ₜ β
μ : Measure α
inst✝ : OuterRegular μ
A : Set β
hA : MeasurableSet A
r : ℝ≥0∞
hr : r > ↑↑μ (↑(Homeomorph.symm f) '' A)
U : Set α
hAU : U ⊇ ↑(Homeomorph.symm f) '' A
hUo : IsOpen U
hU : ↑↑μ U < r
this : IsOpen (↑(Homeomorph.symm f) ⁻¹' U)
⊢ ∃ U, U ⊇ A ∧ IsOpen U ∧ ↑↑(map (↑f) μ) U < r
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace α
μ✝ : Measure α
inst✝⁴ : OpensMeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : BorelSpace β
f : α ≃ₜ β
μ : Measure α
inst✝ : OuterRegular μ
A : Set β
hA : MeasurableSet A
r : ℝ≥0∞
hr : r > ↑↑μ (↑(Homeomorph.symm f) '' A)
U : Set α
hAU : U ⊇ ↑(Homeomorph.symm f) '' A
hUo : IsOpen U
hU : ↑↑μ U < r
⊢ ∃ U, U ⊇ A ∧ IsOpen U ∧ ↑↑(map (↑f) μ) U < r
have : IsOpen (f.symm ⁻¹' U) := hUo.preimage f.symm.continuous
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace α
μ✝ : Measure α
inst✝⁴ : OpensMeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : BorelSpace β
f : α ≃ₜ β
μ : Measure α
inst✝ : OuterRegular μ
A : Set β
hA : MeasurableSet A
r : ℝ≥0∞
hr : r > ↑↑μ (↑(Homeomorph.symm f) '' A)
U : Set α
hAU : U ⊇ ↑(Homeomorph.symm f) '' A
hUo : IsOpen U
hU : ↑↑μ U < r
this : IsOpen (↑(Homeomorph.symm f) ⁻¹' U)
⊢ ↑↑(map (↑f) μ) (↑(Homeomorph.symm f) ⁻¹' U) < r
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace α
μ✝ : Measure α
inst✝⁴ : OpensMeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : BorelSpace β
f : α ≃ₜ β
μ : Measure α
inst✝ : OuterRegular μ
A : Set β
hA : MeasurableSet A
r : ℝ≥0∞
hr : r > ↑↑μ (↑(Homeomorph.symm f) '' A)
U : Set α
hAU : U ⊇ ↑(Homeomorph.symm f) '' A
hUo : IsOpen U
hU : ↑↑μ U < r
this : IsOpen (↑(Homeomorph.symm f) ⁻¹' U)
⊢ ∃ U, U ⊇ A ∧ IsOpen U ∧ ↑↑(map (↑f) μ) U < r
refine' ⟨f.symm ⁻¹' U, image_subset_iff.1 hAU, this, _⟩
no goals
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace α
μ✝ : Measure α
inst✝⁴ : OpensMeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : BorelSpace β
f : α ≃ₜ β
μ : Measure α
inst✝ : OuterRegular μ
A : Set β
hA : MeasurableSet A
r : ℝ≥0∞
hr : r > ↑↑μ (↑(Homeomorph.symm f) '' A)
U : Set α
hAU : U ⊇ ↑(Homeomorph.symm f) '' A
hUo : IsOpen U
hU : ↑↑μ U < r
this : IsOpen (↑(Homeomorph.symm f) ⁻¹' U)
⊢ ↑↑(map (↑f) μ) (↑(Homeomorph.symm f) ⁻¹' U) < r
rwa [map_apply f.measurable this.measurableSet, f.preimage_symm, f.preimage_image]