Ω : Type u_1
inst✝³ : PseudoEMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : SigmaFinite μ
s : Set Ω
a b : ℝ
hab : a < b
mbles : ∀ (r : ℝ), MeasurableSet (frontier (Metric.thickening r s))
⊢ ∃ r, r ∈ Ioo a b ∧ ↑↑μ (frontier (Metric.thickening r s)) = 0
Ω : Type u_1
inst✝³ : PseudoEMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : SigmaFinite μ
s : Set Ω
a b : ℝ
hab : a < b
⊢ ∃ r, r ∈ Ioo a b ∧ ↑↑μ (frontier (Metric.thickening r s)) = 0
have mbles : ∀ r : ℝ, MeasurableSet (frontier (Metric.thickening r s)) :=
  fun r => isClosed_frontier.measurableSet
Ω : Type u_1
inst✝³ : PseudoEMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : SigmaFinite μ
s : Set Ω
a b : ℝ
hab : a < b
mbles : ∀ (r : ℝ), MeasurableSet (frontier (Metric.thickening r s))
disjs : Pairwise (Disjoint on fun r => frontier (Metric.thickening r s))
⊢ ∃ r, r ∈ Ioo a b ∧ ↑↑μ (frontier (Metric.thickening r s)) = 0
Ω : Type u_1
inst✝³ : PseudoEMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : SigmaFinite μ
s : Set Ω
a b : ℝ
hab : a < b
mbles : ∀ (r : ℝ), MeasurableSet (frontier (Metric.thickening r s))
⊢ ∃ r, r ∈ Ioo a b ∧ ↑↑μ (frontier (Metric.thickening r s)) = 0
have disjs := Metric.frontier_thickening_disjoint s
Ω : Type u_1
inst✝³ : PseudoEMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : SigmaFinite μ
s : Set Ω
a b : ℝ
hab : a < b
mbles : ∀ (r : ℝ), MeasurableSet (frontier (Metric.thickening r s))
disjs : Pairwise (Disjoint on fun r => frontier (Metric.thickening r s))
key : Set.Countable {i | 0 < ↑↑μ (frontier (Metric.thickening i s))}
⊢ ∃ r, r ∈ Ioo a b ∧ ↑↑μ (frontier (Metric.thickening r s)) = 0
Ω : Type u_1
inst✝³ : PseudoEMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : SigmaFinite μ
s : Set Ω
a b : ℝ
hab : a < b
mbles : ∀ (r : ℝ), MeasurableSet (frontier (Metric.thickening r s))
disjs : Pairwise (Disjoint on fun r => frontier (Metric.thickening r s))
⊢ ∃ r, r ∈ Ioo a b ∧ ↑↑μ (frontier (Metric.thickening r s)) = 0
have key := @Measure.countable_meas_pos_of_disjoint_iUnion Ω _ _ μ _ _ mbles disjs
Ω : Type u_1
inst✝³ : PseudoEMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : SigmaFinite μ
s : Set Ω
a b : ℝ
hab : a < b
mbles : ∀ (r : ℝ), MeasurableSet (frontier (Metric.thickening r s))
disjs : Pairwise (Disjoint on fun r => frontier (Metric.thickening r s))
key : Set.Countable {i | 0 < ↑↑μ (frontier (Metric.thickening i s))}
aux : ↑↑volume (Ioo a b \ {i | 0 < ↑↑μ (frontier (Metric.thickening i s))}) = ↑↑volume (Ioo a b)
⊢ ∃ r, r ∈ Ioo a b ∧ ↑↑μ (frontier (Metric.thickening r s)) = 0
Ω : Type u_1
inst✝³ : PseudoEMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : SigmaFinite μ
s : Set Ω
a b : ℝ
hab : a < b
mbles : ∀ (r : ℝ), MeasurableSet (frontier (Metric.thickening r s))
disjs : Pairwise (Disjoint on fun r => frontier (Metric.thickening r s))
key : Set.Countable {i | 0 < ↑↑μ (frontier (Metric.thickening i s))}
⊢ ∃ r, r ∈ Ioo a b ∧ ↑↑μ (frontier (Metric.thickening r s)) = 0
have aux := @measure_diff_null ℝ _ volume (Ioo a b) _ (Set.Countable.measure_zero key volume)
Ω : Type u_1
inst✝³ : PseudoEMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : SigmaFinite μ
s : Set Ω
a b : ℝ
hab : a < b
mbles : ∀ (r : ℝ), MeasurableSet (frontier (Metric.thickening r s))
disjs : Pairwise (Disjoint on fun r => frontier (Metric.thickening r s))
key : Set.Countable {i | 0 < ↑↑μ (frontier (Metric.thickening i s))}
aux : ↑↑volume (Ioo a b \ {i | 0 < ↑↑μ (frontier (Metric.thickening i s))}) = ↑↑volume (Ioo a b)
len_pos : 0 < ENNReal.ofReal (b - a)
⊢ ∃ r, r ∈ Ioo a b ∧ ↑↑μ (frontier (Metric.thickening r s)) = 0
Ω : Type u_1
inst✝³ : PseudoEMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : SigmaFinite μ
s : Set Ω
a b : ℝ
hab : a < b
mbles : ∀ (r : ℝ), MeasurableSet (frontier (Metric.thickening r s))
disjs : Pairwise (Disjoint on fun r => frontier (Metric.thickening r s))
key : Set.Countable {i | 0 < ↑↑μ (frontier (Metric.thickening i s))}
aux : ↑↑volume (Ioo a b \ {i | 0 < ↑↑μ (frontier (Metric.thickening i s))}) = ↑↑volume (Ioo a b)
⊢ ∃ r, r ∈ Ioo a b ∧ ↑↑μ (frontier (Metric.thickening r s)) = 0
have len_pos : 0 < ENNReal.ofReal (b - a) := by simp only [hab, ENNReal.ofReal_pos, sub_pos]
Ω : Type u_1
inst✝³ : PseudoEMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : SigmaFinite μ
s : Set Ω
a b : ℝ
hab : a < b
mbles : ∀ (r : ℝ), MeasurableSet (frontier (Metric.thickening r s))
disjs : Pairwise (Disjoint on fun r => frontier (Metric.thickening r s))
key : Set.Countable {i | 0 < ↑↑μ (frontier (Metric.thickening i s))}
aux : ↑↑volume (Ioo a b \ {i | 0 < ↑↑μ (frontier (Metric.thickening i s))}) = ↑↑volume (Ioo a b)
len_pos : 0 < ↑↑volume (Ioo a b \ {i | 0 < ↑↑μ (frontier (Metric.thickening i s))})
⊢ ∃ r, r ∈ Ioo a b ∧ ↑↑μ (frontier (Metric.thickening r s)) = 0
Ω : Type u_1
inst✝³ : PseudoEMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : SigmaFinite μ
s : Set Ω
a b : ℝ
hab : a < b
mbles : ∀ (r : ℝ), MeasurableSet (frontier (Metric.thickening r s))
disjs : Pairwise (Disjoint on fun r => frontier (Metric.thickening r s))
key : Set.Countable {i | 0 < ↑↑μ (frontier (Metric.thickening i s))}
aux : ↑↑volume (Ioo a b \ {i | 0 < ↑↑μ (frontier (Metric.thickening i s))}) = ↑↑volume (Ioo a b)
len_pos : 0 < ENNReal.ofReal (b - a)
⊢ ∃ r, r ∈ Ioo a b ∧ ↑↑μ (frontier (Metric.thickening r s)) = 0
rw [← Real.volume_Ioo, ← aux] at len_pos
case intro.intro
Ω : Type u_1
inst✝³ : PseudoEMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : SigmaFinite μ
s : Set Ω
a b : ℝ
hab : a < b
mbles : ∀ (r : ℝ), MeasurableSet (frontier (Metric.thickening r s))
disjs : Pairwise (Disjoint on fun r => frontier (Metric.thickening r s))
key : Set.Countable {i | 0 < ↑↑μ (frontier (Metric.thickening i s))}
aux : ↑↑volume (Ioo a b \ {i | 0 < ↑↑μ (frontier (Metric.thickening i s))}) = ↑↑volume (Ioo a b)
len_pos : 0 < ↑↑volume (Ioo a b \ {i | 0 < ↑↑μ (frontier (Metric.thickening i s))})
r : ℝ
r_in_Ioo : r ∈ Ioo a b
hr : ¬r ∈ {i | 0 < ↑↑μ (frontier (Metric.thickening i s))}
⊢ ∃ r, r ∈ Ioo a b ∧ ↑↑μ (frontier (Metric.thickening r s)) = 0
Ω : Type u_1
inst✝³ : PseudoEMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : SigmaFinite μ
s : Set Ω
a b : ℝ
hab : a < b
mbles : ∀ (r : ℝ), MeasurableSet (frontier (Metric.thickening r s))
disjs : Pairwise (Disjoint on fun r => frontier (Metric.thickening r s))
key : Set.Countable {i | 0 < ↑↑μ (frontier (Metric.thickening i s))}
aux : ↑↑volume (Ioo a b \ {i | 0 < ↑↑μ (frontier (Metric.thickening i s))}) = ↑↑volume (Ioo a b)
len_pos : 0 < ↑↑volume (Ioo a b \ {i | 0 < ↑↑μ (frontier (Metric.thickening i s))})
⊢ ∃ r, r ∈ Ioo a b ∧ ↑↑μ (frontier (Metric.thickening r s)) = 0
rcases nonempty_of_measure_ne_zero len_pos.ne.symm with ⟨r, ⟨r_in_Ioo, hr⟩⟩
case intro.intro
Ω : Type u_1
inst✝³ : PseudoEMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : SigmaFinite μ
s : Set Ω
a b : ℝ
hab : a < b
mbles : ∀ (r : ℝ), MeasurableSet (frontier (Metric.thickening r s))
disjs : Pairwise (Disjoint on fun r => frontier (Metric.thickening r s))
key : Set.Countable {i | 0 < ↑↑μ (frontier (Metric.thickening i s))}
aux : ↑↑volume (Ioo a b \ {i | 0 < ↑↑μ (frontier (Metric.thickening i s))}) = ↑↑volume (Ioo a b)
len_pos : 0 < ↑↑volume (Ioo a b \ {i | 0 < ↑↑μ (frontier (Metric.thickening i s))})
r : ℝ
r_in_Ioo : r ∈ Ioo a b
hr : ¬r ∈ {i | 0 < ↑↑μ (frontier (Metric.thickening i s))}
⊢ ↑↑μ (frontier (Metric.thickening r s)) = 0
case intro.intro
Ω : Type u_1
inst✝³ : PseudoEMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : SigmaFinite μ
s : Set Ω
a b : ℝ
hab : a < b
mbles : ∀ (r : ℝ), MeasurableSet (frontier (Metric.thickening r s))
disjs : Pairwise (Disjoint on fun r => frontier (Metric.thickening r s))
key : Set.Countable {i | 0 < ↑↑μ (frontier (Metric.thickening i s))}
aux : ↑↑volume (Ioo a b \ {i | 0 < ↑↑μ (frontier (Metric.thickening i s))}) = ↑↑volume (Ioo a b)
len_pos : 0 < ↑↑volume (Ioo a b \ {i | 0 < ↑↑μ (frontier (Metric.thickening i s))})
r : ℝ
r_in_Ioo : r ∈ Ioo a b
hr : ¬r ∈ {i | 0 < ↑↑μ (frontier (Metric.thickening i s))}
⊢ ∃ r, r ∈ Ioo a b ∧ ↑↑μ (frontier (Metric.thickening r s)) = 0
refine' ⟨r, r_in_Ioo, _⟩
no goals
case intro.intro
Ω : Type u_1
inst✝³ : PseudoEMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : SigmaFinite μ
s : Set Ω
a b : ℝ
hab : a < b
mbles : ∀ (r : ℝ), MeasurableSet (frontier (Metric.thickening r s))
disjs : Pairwise (Disjoint on fun r => frontier (Metric.thickening r s))
key : Set.Countable {i | 0 < ↑↑μ (frontier (Metric.thickening i s))}
aux : ↑↑volume (Ioo a b \ {i | 0 < ↑↑μ (frontier (Metric.thickening i s))}) = ↑↑volume (Ioo a b)
len_pos : 0 < ↑↑volume (Ioo a b \ {i | 0 < ↑↑μ (frontier (Metric.thickening i s))})
r : ℝ
r_in_Ioo : r ∈ Ioo a b
hr : ¬r ∈ {i | 0 < ↑↑μ (frontier (Metric.thickening i s))}
⊢ ↑↑μ (frontier (Metric.thickening r s)) = 0
simpa only [mem_setOf_eq, not_lt, le_zero_iff] using hr
no goals
Ω : Type u_1
inst✝³ : PseudoEMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : SigmaFinite μ
s : Set Ω
a b : ℝ
hab : a < b
mbles : ∀ (r : ℝ), MeasurableSet (frontier (Metric.thickening r s))
disjs : Pairwise (Disjoint on fun r => frontier (Metric.thickening r s))
key : Set.Countable {i | 0 < ↑↑μ (frontier (Metric.thickening i s))}
aux : ↑↑volume (Ioo a b \ {i | 0 < ↑↑μ (frontier (Metric.thickening i s))}) = ↑↑volume (Ioo a b)
⊢ 0 < ENNReal.ofReal (b - a)
simp only [hab, ENNReal.ofReal_pos, sub_pos]