From 40fa9ade2f5649569639608db5e621e5fad0cc02 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Sat, 5 Jan 2019 04:49:24 -0500 Subject: [PATCH] fix(analysis/measure_theory): fix build --- analysis/measure_theory/lebesgue_measure.lean | 3 ++- data/real/nnreal.lean | 4 ++++ 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/analysis/measure_theory/lebesgue_measure.lean b/analysis/measure_theory/lebesgue_measure.lean index 51b5c3e991fdc..6137b0de34454 100644 --- a/analysis/measure_theory/lebesgue_measure.lean +++ b/analysis/measure_theory/lebesgue_measure.lean @@ -183,7 +183,8 @@ le_infi $ λ a, le_infi $ λ b, le_infi $ λ h, begin cases le_total a c with hac hca; cases le_total b c with hbc hcb; simp [*, -sub_eq_add_neg, sub_add_sub_cancel']; rw [← ennreal.coe_add, ennreal.coe_le_coe], - { simp [*, nnreal.of_real_add_of_real, -sub_eq_add_neg, sub_add_sub_cancel'] }, + { simp [*, -nnreal.of_real_add, nnreal.of_real_add_of_real, + -sub_eq_add_neg, sub_add_sub_cancel'] }, { rw nnreal.of_real_of_nonpos, { simp }, exact sub_nonpos.2 (le_trans hbc hca) } diff --git a/data/real/nnreal.lean b/data/real/nnreal.lean index 5233eb170eb12..a8f78fb4b3f04 100644 --- a/data/real/nnreal.lean +++ b/data/real/nnreal.lean @@ -268,6 +268,10 @@ of_real_lt_of_real_iff'.trans (and_iff_left h) nnreal.of_real (r + p) = nnreal.of_real r + nnreal.of_real p := nnreal.eq $ by simp [nnreal.of_real, hr, hp, add_nonneg] +lemma of_real_add_of_real {r p : ℝ} (hr : 0 ≤ r) (hp : 0 ≤ p) : + nnreal.of_real r + nnreal.of_real p = nnreal.of_real (r + p) := +(of_real_add hr hp).symm + lemma of_real_le_of_real {r p : ℝ} (h : r ≤ p) : nnreal.of_real r ≤ nnreal.of_real p := nnreal.coe_le.2 $ max_le_max h $ le_refl _