diff --git a/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean b/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean
index 181c195b09972..c68d79aaeb4eb 100644
--- a/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean
+++ b/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean
@@ -12,7 +12,6 @@ import Mathlib.Analysis.Normed.Group.Basic
 import Mathlib.MeasureTheory.Function.AEMeasurableSequence
 import Mathlib.MeasureTheory.Group.Arithmetic
 import Mathlib.MeasureTheory.Lattice
-import Mathlib.MeasureTheory.Measure.OpenPos
 import Mathlib.Topology.Algebra.Order.LiminfLimsup
 import Mathlib.Topology.ContinuousFunction.Basic
 import Mathlib.Topology.Instances.EReal
@@ -839,14 +838,6 @@ theorem ClosedEmbedding.measurable {f : α → γ} (hf : ClosedEmbedding f) : Me
   hf.continuous.measurable
 #align closed_embedding.measurable ClosedEmbedding.measurable
 
-theorem Continuous.isOpenPosMeasure_map {f : β → γ} (hf : Continuous f)
-    (hf_surj : Function.Surjective f) {μ : Measure β} [μ.IsOpenPosMeasure] :
-    (Measure.map f μ).IsOpenPosMeasure := by
-  refine' ⟨fun U hUo hUne => _⟩
-  rw [Measure.map_apply hf.measurable hUo.measurableSet]
-  exact (hUo.preimage hf).measure_ne_zero μ (hf_surj.nonempty_preimage.mpr hUne)
-#align continuous.is_open_pos_measure_map Continuous.isOpenPosMeasure_map
-
 /-- If a function is defined piecewise in terms of functions which are continuous on their
 respective pieces, then it is measurable. -/
 theorem ContinuousOn.measurable_piecewise {f g : α → γ} {s : Set α} [∀ j : α, Decidable (j ∈ s)]
diff --git a/Mathlib/MeasureTheory/Function/LpSpace.lean b/Mathlib/MeasureTheory/Function/LpSpace.lean
index 257d3ac2e917e..3f2e750dd0750 100644
--- a/Mathlib/MeasureTheory/Function/LpSpace.lean
+++ b/Mathlib/MeasureTheory/Function/LpSpace.lean
@@ -10,6 +10,7 @@ Authors: Rémy Degenne, Sébastien Gouëzel
 -/
 import Mathlib.Analysis.Normed.Group.Hom
 import Mathlib.MeasureTheory.Function.LpSeminorm
+import Mathlib.MeasureTheory.Measure.OpenPos
 import Mathlib.Topology.ContinuousFunction.Compact
 
 /-!
diff --git a/Mathlib/MeasureTheory/Measure/OpenPos.lean b/Mathlib/MeasureTheory/Measure/OpenPos.lean
index fd82faa5e0a13..959498b0612e2 100644
--- a/Mathlib/MeasureTheory/Measure/OpenPos.lean
+++ b/Mathlib/MeasureTheory/Measure/OpenPos.lean
@@ -9,6 +9,7 @@ Authors: Yury Kudryashov
 ! if you have ported upstream changes.
 -/
 import Mathlib.MeasureTheory.Measure.MeasureSpace
+import Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
 
 /-!
 # Measures positive on nonempty opens
@@ -39,7 +40,7 @@ class IsOpenPosMeasure : Prop where
   open_pos : ∀ U : Set X, IsOpen U → U.Nonempty → μ U ≠ 0
 #align measure_theory.measure.is_open_pos_measure MeasureTheory.Measure.IsOpenPosMeasure
 
-variable [IsOpenPosMeasure μ] {s U : Set X} {x : X}
+variable [IsOpenPosMeasure μ] {s U F : Set X} {x : X}
 
 theorem _root_.IsOpen.measure_ne_zero (hU : IsOpen U) (hne : U.Nonempty) : μ U ≠ 0 :=
   IsOpenPosMeasure.open_pos U hU hne
@@ -80,10 +81,33 @@ theorem _root_.LE.le.isOpenPosMeasure (h : μ ≤ ν) : IsOpenPosMeasure ν :=
   h.absolutelyContinuous.isOpenPosMeasure
 #align has_le.le.is_open_pos_measure LE.le.isOpenPosMeasure
 
+theorem _root_.IsOpen.measure_zero_iff_eq_empty (hU : IsOpen U) :
+    μ U = 0 ↔ U = ∅ :=
+  ⟨fun h ↦ (hU.measure_eq_zero_iff μ).mp h, fun h ↦ by simp [h]⟩
+
+theorem _root_.IsOpen.ae_eq_empty_iff_eq (hU : IsOpen U) :
+    U =ᵐ[μ] (∅ : Set X) ↔ U = ∅ := by
+  rw [ae_eq_empty, hU.measure_zero_iff_eq_empty]
+
 theorem _root_.IsOpen.eq_empty_of_measure_zero (hU : IsOpen U) (h₀ : μ U = 0) : U = ∅ :=
   (hU.measure_eq_zero_iff μ).mp h₀
 #align is_open.eq_empty_of_measure_zero IsOpen.eq_empty_of_measure_zero
 
+theorem _root_.IsClosed.ae_eq_univ_iff_eq (hF : IsClosed F) :
+    F =ᵐ[μ] univ ↔ F = univ := by
+  refine' ⟨fun h ↦ _, fun h ↦ by rw [h]⟩
+  rwa [ae_eq_univ, hF.isOpen_compl.measure_eq_zero_iff μ, compl_empty_iff] at h
+
+theorem _root_.IsClosed.measure_eq_univ_iff_eq [OpensMeasurableSpace X] [IsFiniteMeasure μ]
+    (hF : IsClosed F) :
+    μ F = μ univ ↔ F = univ := by
+  rw [← ae_eq_univ_iff_measure_eq hF.measurableSet.nullMeasurableSet, hF.ae_eq_univ_iff_eq]
+
+theorem _root_.IsClosed.measure_eq_one_iff_eq_univ [OpensMeasurableSpace X] [IsProbabilityMeasure μ]
+    (hF : IsClosed F) :
+    μ F = 1 ↔ F = univ := by
+  rw [← measure_univ (μ := μ), hF.measure_eq_univ_iff_eq]
+
 theorem interior_eq_empty_of_null (hs : μ s = 0) : interior s = ∅ :=
   isOpen_interior.eq_empty_of_measure_zero <| measure_mono_null interior_subset hs
 #align measure_theory.measure.interior_eq_empty_of_null MeasureTheory.Measure.interior_eq_empty_of_null
@@ -125,6 +149,17 @@ theorem _root_.Continuous.ae_eq_iff_eq {f g : X → Y} (hf : Continuous f) (hg :
   ⟨fun h => eq_of_ae_eq h hf hg, fun h => h ▸ EventuallyEq.rfl⟩
 #align continuous.ae_eq_iff_eq Continuous.ae_eq_iff_eq
 
+variable {μ}
+
+theorem _root_.Continuous.isOpenPosMeasure_map [OpensMeasurableSpace X]
+    {Z : Type _} [TopologicalSpace Z] [MeasurableSpace Z] [BorelSpace Z]
+    {f : X → Z} (hf : Continuous f) (hf_surj : Function.Surjective f) :
+    (Measure.map f μ).IsOpenPosMeasure := by
+  refine' ⟨fun U hUo hUne => _⟩
+  rw [Measure.map_apply hf.measurable hUo.measurableSet]
+  exact (hUo.preimage hf).measure_ne_zero μ (hf_surj.nonempty_preimage.mpr hUne)
+#align continuous.is_open_pos_measure_map Continuous.isOpenPosMeasure_map
+
 end Basic
 
 section LinearOrder