α : Type u_1
β : Type ?u.24581
γ : Type ?u.24584
δ : Type ?u.24587
ι : Type ?u.24590
R : Type ?u.24593
R' : Type ?u.24596
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
hs : MeasurableSet s
hst : s ⊆ t
hs' : ↑↑μ s ≠ ⊤
ε : ℝ≥0∞
h : ↑↑μ t < ↑↑μ s + ε
⊢ ↑↑μ t - ↑↑μ s < ε
α : Type u_1
β : Type ?u.24581
γ : Type ?u.24584
δ : Type ?u.24587
ι : Type ?u.24590
R : Type ?u.24593
R' : Type ?u.24596
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
hs : MeasurableSet s
hst : s ⊆ t
hs' : ↑↑μ s ≠ ⊤
ε : ℝ≥0∞
h : ↑↑μ t < ↑↑μ s + ε
⊢ ↑↑μ (t \ s) < ε
rw [measure_diff hst hs hs']
α : Type u_1
β : Type ?u.24581
γ : Type ?u.24584
δ : Type ?u.24587
ι : Type ?u.24590
R : Type ?u.24593
R' : Type ?u.24596
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
hs : MeasurableSet s
hst : s ⊆ t
hs' : ↑↑μ s ≠ ⊤
ε : ℝ≥0∞
h : ↑↑μ t < ε + ↑↑μ s
⊢ ↑↑μ t - ↑↑μ s < ε
α : Type u_1
β : Type ?u.24581
γ : Type ?u.24584
δ : Type ?u.24587
ι : Type ?u.24590
R : Type ?u.24593
R' : Type ?u.24596
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
hs : MeasurableSet s
hst : s ⊆ t
hs' : ↑↑μ s ≠ ⊤
ε : ℝ≥0∞
h : ↑↑μ t < ↑↑μ s + ε
⊢ ↑↑μ t - ↑↑μ s < ε
rw [add_comm] at h
no goals
α : Type u_1
β : Type ?u.24581
γ : Type ?u.24584
δ : Type ?u.24587
ι : Type ?u.24590
R : Type ?u.24593
R' : Type ?u.24596
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
hs : MeasurableSet s
hst : s ⊆ t
hs' : ↑↑μ s ≠ ⊤
ε : ℝ≥0∞
h : ↑↑μ t < ε + ↑↑μ s
⊢ ↑↑μ t - ↑↑μ s < ε
exact ENNReal.sub_lt_of_lt_add (measure_mono hst) h