move ae_ne_bot.to_ne_zero

leanprover-community · Aug 3, 2023 · a937abb · a937abb
1 parent 6b4eb9d
commit a937abb
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 4 deletions.
diff --git a/src/measure_theory/measure/lebesgue/eq_haar.lean b/src/measure_theory/measure/lebesgue/eq_haar.lean
@@ -111,10 +111,6 @@ variables {H : Type*} [measurable_space H] [seminormed_group H] [opens_measurabl
 
 open metric
 
-instance ae_ne_bot.to_ne_zero {α : Type*} [measurable_space α] [nonempty α] {μ : measure α}
-  [μ.ae.ne_bot] : ne_zero μ :=
-⟨ae_ne_bot.1 ‹_›⟩
-
 @[to_additive]
 lemma _root_.measurable.exists_nhds_one_bounded (f : G →* H) (h : measurable f)
   (μ : measure G . volume_tac) [μ.is_haar_measure] :

diff --git a/src/measure_theory/measure/measure_space.lean b/src/measure_theory/measure/measure_space.lean
@@ -2329,6 +2329,8 @@ by rw [← empty_mem_iff_bot, mem_ae_iff, compl_empty, measure_univ_eq_zero]
 @[simp] lemma ae_ne_bot : μ.ae.ne_bot ↔ μ ≠ 0 :=
 ne_bot_iff.trans (not_congr ae_eq_bot)
 
+instance ae_ne_bot.to_ne_zero [μ.ae.ne_bot] : ne_zero μ := ⟨ae_ne_bot.1 ‹_›⟩
+
 @[simp] lemma ae_zero {m0 : measurable_space α} : (0 : measure α).ae = ⊥ := ae_eq_bot.2 rfl
 
 @[mono] lemma ae_mono (h : μ ≤ ν) : μ.ae ≤ ν.ae := h.absolutely_continuous.ae_le