From 62755cf6315d13f811e1829ef7d27ccea3436fae Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Sat, 27 Jun 2020 00:16:24 -0400 Subject: [PATCH] instantiate general lemmas --- src/measure_theory/outer_measure.lean | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/measure_theory/outer_measure.lean b/src/measure_theory/outer_measure.lean index c15ad3d089825..f2b0c5f140b77 100644 --- a/src/measure_theory/outer_measure.lean +++ b/src/measure_theory/outer_measure.lean @@ -63,7 +63,7 @@ namespace outer_measure section basic -variables {α : Type*} {ms : set (outer_measure α)} {m : outer_measure α} +variables {α : Type*} {β : Type*} {ms : set (outer_measure α)} {m : outer_measure α} instance : has_coe_to_fun (outer_measure α) := ⟨_, λ m, m.measure_of⟩ @@ -77,19 +77,19 @@ theorem mono' (m : outer_measure α) {s₁ s₂} protected theorem Union (m : outer_measure α) {β} [encodable β] (s : β → set α) : m (⋃i, s i) ≤ (∑'i, m (s i)) := -by rw [Union_decode2, tsum_Union_decode2 _ m.empty' s]; exact m.Union_nat _ +supr_R_tsum m m.empty (≤) m.Union_nat s lemma Union_null (m : outer_measure α) {β} [encodable β] {s : β → set α} (h : ∀ i, m (s i) = 0) : m (⋃i, s i) = 0 := by simpa [h] using m.Union s +protected lemma Union_finset (m : outer_measure α) (s : β → set α) (t : finset β) : + m (⋃i ∈ t, s i) ≤ t.sum (λ d, m (s d)) := +supr_R_sum m m.empty (≤) m.Union_nat s t + protected lemma union (m : outer_measure α) (s₁ s₂ : set α) : m (s₁ ∪ s₂) ≤ m s₁ + m s₂ := -begin - convert m.Union (λ b, cond b s₁ s₂), - { simp [union_eq_Union] }, - { rw tsum_fintype, change _ = _ + _, simp } -end +sup_R_add m m.empty (≤) m.Union_nat s₁ s₂ lemma le_inter_add_diff {m : outer_measure α} {t : set α} (s : set α) : m t ≤ m (t ∩ s) + m (t \ s) :=