[GOAL]
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
m : MeasurableSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
μ ν : Measure X
inst✝ : IsOpenPosMeasure μ
s U F : Set X
x : X
hU : IsOpen U
⊢ ↑↑μ U = 0 ↔ U = ∅
[PROOFSTEP]
simpa only [not_lt, nonpos_iff_eq_zero, not_nonempty_iff_eq_empty] using not_congr (hU.measure_pos_iff μ)
[GOAL]
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
m : MeasurableSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
μ ν : Measure X
inst✝ : IsOpenPosMeasure μ
s U F : Set X
x : X
hU : IsOpen U
h : U = ∅
⊢ ↑↑μ U = 0
[PROOFSTEP]
simp [h]
[GOAL]
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
m : MeasurableSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
μ ν : Measure X
inst✝ : IsOpenPosMeasure μ
s U F : Set X
x : X
hU : IsOpen U
⊢ U =ᶠ[ae μ] ∅ ↔ U = ∅
[PROOFSTEP]
rw [ae_eq_empty, hU.measure_zero_iff_eq_empty]
[GOAL]
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
m : MeasurableSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
μ ν : Measure X
inst✝ : IsOpenPosMeasure μ
s U F : Set X
x : X
hF : IsClosed F
⊢ F =ᶠ[ae μ] univ ↔ F = univ
[PROOFSTEP]
refine' ⟨fun h ↦ _, fun h ↦ by rw [h]⟩
[GOAL]
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
m : MeasurableSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
μ ν : Measure X
inst✝ : IsOpenPosMeasure μ
s U F : Set X
x : X
hF : IsClosed F
h : F = univ
⊢ F =ᶠ[ae μ] univ
[PROOFSTEP]
rw [h]
[GOAL]
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
m : MeasurableSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
μ ν : Measure X
inst✝ : IsOpenPosMeasure μ
s U F : Set X
x : X
hF : IsClosed F
h : F =ᶠ[ae μ] univ
⊢ F = univ
[PROOFSTEP]
rwa [ae_eq_univ, hF.isOpen_compl.measure_eq_zero_iff μ, compl_empty_iff] at h 
[GOAL]
X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
m : MeasurableSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : T2Space Y
μ ν : Measure X
inst✝² : IsOpenPosMeasure μ
s U F : Set X
x : X
inst✝¹ : OpensMeasurableSpace X
inst✝ : IsFiniteMeasure μ
hF : IsClosed F
⊢ ↑↑μ F = ↑↑μ univ ↔ F = univ
[PROOFSTEP]
rw [← ae_eq_univ_iff_measure_eq hF.measurableSet.nullMeasurableSet, hF.ae_eq_univ_iff_eq]
[GOAL]
X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
m : MeasurableSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : T2Space Y
μ ν : Measure X
inst✝² : IsOpenPosMeasure μ
s U F : Set X
x : X
inst✝¹ : OpensMeasurableSpace X
inst✝ : IsProbabilityMeasure μ
hF : IsClosed F
⊢ ↑↑μ F = 1 ↔ F = univ
[PROOFSTEP]
rw [← measure_univ (μ := μ), hF.measure_eq_univ_iff_eq]
[GOAL]
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
m : MeasurableSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
μ ν : Measure X
inst✝ : IsOpenPosMeasure μ
s U F : Set X
x : X
f g : X → Y
h : f =ᶠ[ae (restrict μ U)] g
hU : IsOpen U
hf : ContinuousOn f U
hg : ContinuousOn g U
⊢ EqOn f g U
[PROOFSTEP]
replace h := ae_imp_of_ae_restrict h
[GOAL]
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
m : MeasurableSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
μ ν : Measure X
inst✝ : IsOpenPosMeasure μ
s U F : Set X
x : X
f g : X → Y
hU : IsOpen U
hf : ContinuousOn f U
hg : ContinuousOn g U
h : ∀ᵐ (x : X) ∂μ, x ∈ U → f x = g x
⊢ EqOn f g U
[PROOFSTEP]
simp only [EventuallyEq, ae_iff, not_imp] at h 
[GOAL]
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
m : MeasurableSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
μ ν : Measure X
inst✝ : IsOpenPosMeasure μ
s U F : Set X
x : X
f g : X → Y
hU : IsOpen U
hf : ContinuousOn f U
hg : ContinuousOn g U
h : ↑↑μ {a | a ∈ U ∧ ¬f a = g a} = 0
⊢ EqOn f g U
[PROOFSTEP]
have : IsOpen (U ∩ {a | f a ≠ g a}) :=
  by
  refine' isOpen_iff_mem_nhds.mpr fun a ha => inter_mem (hU.mem_nhds ha.1) _
  rcases ha with ⟨ha : a ∈ U, ha' : (f a, g a) ∈ (diagonal Y)ᶜ⟩
  exact
    (hf.continuousAt (hU.mem_nhds ha)).prod_mk_nhds (hg.continuousAt (hU.mem_nhds ha))
      (isClosed_diagonal.isOpen_compl.mem_nhds ha')
[GOAL]
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
m : MeasurableSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
μ ν : Measure X
inst✝ : IsOpenPosMeasure μ
s U F : Set X
x : X
f g : X → Y
hU : IsOpen U
hf : ContinuousOn f U
hg : ContinuousOn g U
h : ↑↑μ {a | a ∈ U ∧ ¬f a = g a} = 0
⊢ IsOpen (U ∩ {a | f a ≠ g a})
[PROOFSTEP]
refine' isOpen_iff_mem_nhds.mpr fun a ha => inter_mem (hU.mem_nhds ha.1) _
[GOAL]
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
m : MeasurableSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
μ ν : Measure X
inst✝ : IsOpenPosMeasure μ
s U F : Set X
x : X
f g : X → Y
hU : IsOpen U
hf : ContinuousOn f U
hg : ContinuousOn g U
h : ↑↑μ {a | a ∈ U ∧ ¬f a = g a} = 0
a : X
ha : a ∈ U ∩ {a | f a ≠ g a}
⊢ {a | f a ≠ g a} ∈ 𝓝 a
[PROOFSTEP]
rcases ha with ⟨ha : a ∈ U, ha' : (f a, g a) ∈ (diagonal Y)ᶜ⟩
[GOAL]
case intro
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
m : MeasurableSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
μ ν : Measure X
inst✝ : IsOpenPosMeasure μ
s U F : Set X
x : X
f g : X → Y
hU : IsOpen U
hf : ContinuousOn f U
hg : ContinuousOn g U
h : ↑↑μ {a | a ∈ U ∧ ¬f a = g a} = 0
a : X
ha : a ∈ U
ha' : (f a, g a) ∈ (diagonal Y)ᶜ
⊢ {a | f a ≠ g a} ∈ 𝓝 a
[PROOFSTEP]
exact
  (hf.continuousAt (hU.mem_nhds ha)).prod_mk_nhds (hg.continuousAt (hU.mem_nhds ha))
    (isClosed_diagonal.isOpen_compl.mem_nhds ha')
[GOAL]
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
m : MeasurableSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
μ ν : Measure X
inst✝ : IsOpenPosMeasure μ
s U F : Set X
x : X
f g : X → Y
hU : IsOpen U
hf : ContinuousOn f U
hg : ContinuousOn g U
h : ↑↑μ {a | a ∈ U ∧ ¬f a = g a} = 0
this : IsOpen (U ∩ {a | f a ≠ g a})
⊢ EqOn f g U
[PROOFSTEP]
replace := (this.eq_empty_of_measure_zero h).le
[GOAL]
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
m : MeasurableSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
μ ν : Measure X
inst✝ : IsOpenPosMeasure μ
s U F : Set X
x : X
f g : X → Y
hU : IsOpen U
hf : ContinuousOn f U
hg : ContinuousOn g U
h : ↑↑μ {a | a ∈ U ∧ ¬f a = g a} = 0
this : U ∩ {a | f a ≠ g a} ≤ ∅
⊢ EqOn f g U
[PROOFSTEP]
exact fun x hx => Classical.not_not.1 fun h => this ⟨hx, h⟩
[GOAL]
X : Type u_1
Y : Type u_2
inst✝⁷ : TopologicalSpace X
m : MeasurableSpace X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : T2Space Y
μ ν : Measure X
inst✝⁴ : IsOpenPosMeasure μ
s U F : Set X
x : X
inst✝³ : OpensMeasurableSpace X
Z : Type u_3
inst✝² : TopologicalSpace Z
inst✝¹ : MeasurableSpace Z
inst✝ : BorelSpace Z
f : X → Z
hf : Continuous f
hf_surj : Surjective f
⊢ IsOpenPosMeasure (map f μ)
[PROOFSTEP]
refine' ⟨fun U hUo hUne => _⟩
[GOAL]
X : Type u_1
Y : Type u_2
inst✝⁷ : TopologicalSpace X
m : MeasurableSpace X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : T2Space Y
μ ν : Measure X
inst✝⁴ : IsOpenPosMeasure μ
s U✝ F : Set X
x : X
inst✝³ : OpensMeasurableSpace X
Z : Type u_3
inst✝² : TopologicalSpace Z
inst✝¹ : MeasurableSpace Z
inst✝ : BorelSpace Z
f : X → Z
hf : Continuous f
hf_surj : Surjective f
U : Set Z
hUo : IsOpen U
hUne : Set.Nonempty U
⊢ ↑↑(map f μ) U ≠ 0
[PROOFSTEP]
rw [Measure.map_apply hf.measurable hUo.measurableSet]
[GOAL]
X : Type u_1
Y : Type u_2
inst✝⁷ : TopologicalSpace X
m : MeasurableSpace X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : T2Space Y
μ ν : Measure X
inst✝⁴ : IsOpenPosMeasure μ
s U✝ F : Set X
x : X
inst✝³ : OpensMeasurableSpace X
Z : Type u_3
inst✝² : TopologicalSpace Z
inst✝¹ : MeasurableSpace Z
inst✝ : BorelSpace Z
f : X → Z
hf : Continuous f
hf_surj : Surjective f
U : Set Z
hUo : IsOpen U
hUne : Set.Nonempty U
⊢ ↑↑μ (f ⁻¹' U) ≠ 0
[PROOFSTEP]
exact (hUo.preimage hf).measure_ne_zero μ (hf_surj.nonempty_preimage.mpr hUne)
[GOAL]
X✝ : Type u_1
inst✝⁴ : PseudoMetricSpace X✝
m✝ : MeasurableSpace X✝
μ✝ : Measure X✝
inst✝³ : IsOpenPosMeasure μ✝
X : Type u_2
inst✝² : MetricSpace X
m : MeasurableSpace X
μ : Measure X
inst✝¹ : IsOpenPosMeasure μ
inst✝ : NoAtoms μ
x : X
r : ℝ
⊢ 0 < ↑↑μ (closedBall x r) ↔ 0 < r
[PROOFSTEP]
refine' ⟨fun h ↦ _, measure_closedBall_pos μ x⟩
[GOAL]
X✝ : Type u_1
inst✝⁴ : PseudoMetricSpace X✝
m✝ : MeasurableSpace X✝
μ✝ : Measure X✝
inst✝³ : IsOpenPosMeasure μ✝
X : Type u_2
inst✝² : MetricSpace X
m : MeasurableSpace X
μ : Measure X
inst✝¹ : IsOpenPosMeasure μ
inst✝ : NoAtoms μ
x : X
r : ℝ
h : 0 < ↑↑μ (closedBall x r)
⊢ 0 < r
[PROOFSTEP]
contrapose! h
[GOAL]
X✝ : Type u_1
inst✝⁴ : PseudoMetricSpace X✝
m✝ : MeasurableSpace X✝
μ✝ : Measure X✝
inst✝³ : IsOpenPosMeasure μ✝
X : Type u_2
inst✝² : MetricSpace X
m : MeasurableSpace X
μ : Measure X
inst✝¹ : IsOpenPosMeasure μ
inst✝ : NoAtoms μ
x : X
r : ℝ
h : r ≤ 0
⊢ ↑↑μ (closedBall x r) ≤ 0
[PROOFSTEP]
rw [(subsingleton_closedBall x h).measure_zero μ]
