chore(measure_theory): add 2 lemmas (#9329)

leanprover-community · Sep 22, 2021 · c9638b9 · c9638b9
1 parent 6f2cbde
commit c9638b9
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 0 deletions.
diff --git a/src/measure_theory/measure/measure_space.lean b/src/measure_theory/measure/measure_space.lean
@@ -394,6 +394,10 @@ m.le_trim s
   μ.to_outer_measure.to_measure (le_to_outer_measure_caratheodory _) = μ :=
 measure.ext $ λ s, μ.to_outer_measure.trim_eq
 
+@[simp] lemma bounded_by_measure (μ : measure α) :
+  outer_measure.bounded_by μ = μ.to_outer_measure :=
+μ.to_outer_measure.bounded_by_eq_self
+
 end outer_measure
 
 variables {m0 : measurable_space α} [measurable_space β] [measurable_space γ]

diff --git a/src/measure_theory/measure/outer_measure.lean b/src/measure_theory/measure/outer_measure.lean
@@ -602,6 +602,9 @@ theorem bounded_by_eq (s : set α) (m_empty : m ∅ = 0) (m_mono : ∀ ⦃t : se
   (m_subadd : ∀ (s : ℕ → set α), m (⋃i, s i) ≤ ∑'i, m (s i)) : bounded_by m s = m s :=
 by rw [bounded_by_eq_of_function m_empty, of_function_eq s m_mono m_subadd]
 
+@[simp] theorem bounded_by_eq_self (m : outer_measure α) : bounded_by m = m :=
+ext $ λ s, bounded_by_eq _ m.empty' (λ t ht, m.mono' ht) m.Union
+
 theorem le_bounded_by {μ : outer_measure α} : μ ≤ bounded_by m ↔ ∀ s, μ s ≤ m s :=
 begin
   rw [bounded_by, le_of_function, forall_congr], intro s,