α : Type u_1
β : Type ?u.2091678
γ : Type ?u.2091681
γ₂ : Type ?u.2091684
δ : Type ?u.2091687
ι : Sort y
s✝ t u : Set α
inst✝³ : PseudoMetricSpace α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
inst✝ : MeasurableSpace β
x : α
ε : ℝ
μ : MeasureTheory.Measure α
s : Set α
hs : ∃ R, R > 0 ∧ ↑↑μ (cthickening R s) ≠ ⊤
A : Tendsto (fun r => ↑↑μ (cthickening r s)) (𝓝[Ioi 0] 0) (𝓝 (↑↑μ (closure s)))
⊢ Tendsto (fun r => ↑↑μ (cthickening r s)) (𝓝 0) (𝓝 (↑↑μ (closure s)))
α : Type u_1
β : Type ?u.2091678
γ : Type ?u.2091681
γ₂ : Type ?u.2091684
δ : Type ?u.2091687
ι : Sort y
s✝ t u : Set α
inst✝³ : PseudoMetricSpace α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
inst✝ : MeasurableSpace β
x : α
ε : ℝ
μ : MeasureTheory.Measure α
s : Set α
hs : ∃ R, R > 0 ∧ ↑↑μ (cthickening R s) ≠ ⊤
⊢ Tendsto (fun r => ↑↑μ (cthickening r s)) (𝓝 0) (𝓝 (↑↑μ (closure s)))
have A : Tendsto (fun r => μ (cthickening r s)) (𝓝[Ioi 0] 0) (𝓝 (μ (closure s))) := by
  rw [closure_eq_iInter_cthickening]
  exact
    tendsto_measure_biInter_gt (fun r _ => isClosed_cthickening.measurableSet)
      (fun i j _ ij => cthickening_mono ij _) hs
α : Type u_1
β : Type ?u.2091678
γ : Type ?u.2091681
γ₂ : Type ?u.2091684
δ : Type ?u.2091687
ι : Sort y
s✝ t u : Set α
inst✝³ : PseudoMetricSpace α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
inst✝ : MeasurableSpace β
x : α
ε : ℝ
μ : MeasureTheory.Measure α
s : Set α
hs : ∃ R, R > 0 ∧ ↑↑μ (cthickening R s) ≠ ⊤
A : Tendsto (fun r => ↑↑μ (cthickening r s)) (𝓝[Ioi 0] 0) (𝓝 (↑↑μ (closure s)))
B : Tendsto (fun r => ↑↑μ (cthickening r s)) (𝓝[Iic 0] 0) (𝓝 (↑↑μ (closure s)))
⊢ Tendsto (fun r => ↑↑μ (cthickening r s)) (𝓝 0) (𝓝 (↑↑μ (closure s)))
α : Type u_1
β : Type ?u.2091678
γ : Type ?u.2091681
γ₂ : Type ?u.2091684
δ : Type ?u.2091687
ι : Sort y
s✝ t u : Set α
inst✝³ : PseudoMetricSpace α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
inst✝ : MeasurableSpace β
x : α
ε : ℝ
μ : MeasureTheory.Measure α
s : Set α
hs : ∃ R, R > 0 ∧ ↑↑μ (cthickening R s) ≠ ⊤
A : Tendsto (fun r => ↑↑μ (cthickening r s)) (𝓝[Ioi 0] 0) (𝓝 (↑↑μ (closure s)))
⊢ Tendsto (fun r => ↑↑μ (cthickening r s)) (𝓝 0) (𝓝 (↑↑μ (closure s)))
have B : Tendsto (fun r => μ (cthickening r s)) (𝓝[Iic 0] 0) (𝓝 (μ (closure s))) := by
  apply Tendsto.congr' _ tendsto_const_nhds
  filter_upwards [self_mem_nhdsWithin (α := ℝ)] with _ hr
  rw [cthickening_of_nonpos hr]
case h.e'_4
α : Type u_1
β : Type ?u.2091678
γ : Type ?u.2091681
γ₂ : Type ?u.2091684
δ : Type ?u.2091687
ι : Sort y
s✝ t u : Set α
inst✝³ : PseudoMetricSpace α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
inst✝ : MeasurableSpace β
x : α
ε : ℝ
μ : MeasureTheory.Measure α
s : Set α
hs : ∃ R, R > 0 ∧ ↑↑μ (cthickening R s) ≠ ⊤
A : Tendsto (fun r => ↑↑μ (cthickening r s)) (𝓝[Ioi 0] 0) (𝓝 (↑↑μ (closure s)))
B : Tendsto (fun r => ↑↑μ (cthickening r s)) (𝓝[Iic 0] 0) (𝓝 (↑↑μ (closure s)))
⊢ 𝓝 0 = 𝓝[Iic 0] 0 ⊔ 𝓝[Ioi 0] 0
α : Type u_1
β : Type ?u.2091678
γ : Type ?u.2091681
γ₂ : Type ?u.2091684
δ : Type ?u.2091687
ι : Sort y
s✝ t u : Set α
inst✝³ : PseudoMetricSpace α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
inst✝ : MeasurableSpace β
x : α
ε : ℝ
μ : MeasureTheory.Measure α
s : Set α
hs : ∃ R, R > 0 ∧ ↑↑μ (cthickening R s) ≠ ⊤
A : Tendsto (fun r => ↑↑μ (cthickening r s)) (𝓝[Ioi 0] 0) (𝓝 (↑↑μ (closure s)))
B : Tendsto (fun r => ↑↑μ (cthickening r s)) (𝓝[Iic 0] 0) (𝓝 (↑↑μ (closure s)))
⊢ Tendsto (fun r => ↑↑μ (cthickening r s)) (𝓝 0) (𝓝 (↑↑μ (closure s)))
convert B.sup A
no goals
case h.e'_4
α : Type u_1
β : Type ?u.2091678
γ : Type ?u.2091681
γ₂ : Type ?u.2091684
δ : Type ?u.2091687
ι : Sort y
s✝ t u : Set α
inst✝³ : PseudoMetricSpace α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
inst✝ : MeasurableSpace β
x : α
ε : ℝ
μ : MeasureTheory.Measure α
s : Set α
hs : ∃ R, R > 0 ∧ ↑↑μ (cthickening R s) ≠ ⊤
A : Tendsto (fun r => ↑↑μ (cthickening r s)) (𝓝[Ioi 0] 0) (𝓝 (↑↑μ (closure s)))
B : Tendsto (fun r => ↑↑μ (cthickening r s)) (𝓝[Iic 0] 0) (𝓝 (↑↑μ (closure s)))
⊢ 𝓝 0 = 𝓝[Iic 0] 0 ⊔ 𝓝[Ioi 0] 0
exact (nhds_left_sup_nhds_right' 0).symm
α : Type u_1
β : Type ?u.2091678
γ : Type ?u.2091681
γ₂ : Type ?u.2091684
δ : Type ?u.2091687
ι : Sort y
s✝ t u : Set α
inst✝³ : PseudoMetricSpace α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
inst✝ : MeasurableSpace β
x : α
ε : ℝ
μ : MeasureTheory.Measure α
s : Set α
hs : ∃ R, R > 0 ∧ ↑↑μ (cthickening R s) ≠ ⊤
⊢ Tendsto (fun r => ↑↑μ (cthickening r s)) (𝓝[Ioi 0] 0) (𝓝 (↑↑μ (⋂ (δ : ℝ) (_ : 0 < δ), cthickening δ s)))
α : Type u_1
β : Type ?u.2091678
γ : Type ?u.2091681
γ₂ : Type ?u.2091684
δ : Type ?u.2091687
ι : Sort y
s✝ t u : Set α
inst✝³ : PseudoMetricSpace α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
inst✝ : MeasurableSpace β
x : α
ε : ℝ
μ : MeasureTheory.Measure α
s : Set α
hs : ∃ R, R > 0 ∧ ↑↑μ (cthickening R s) ≠ ⊤
⊢ Tendsto (fun r => ↑↑μ (cthickening r s)) (𝓝[Ioi 0] 0) (𝓝 (↑↑μ (closure s)))
rw [closure_eq_iInter_cthickening]
no goals
α : Type u_1
β : Type ?u.2091678
γ : Type ?u.2091681
γ₂ : Type ?u.2091684
δ : Type ?u.2091687
ι : Sort y
s✝ t u : Set α
inst✝³ : PseudoMetricSpace α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
inst✝ : MeasurableSpace β
x : α
ε : ℝ
μ : MeasureTheory.Measure α
s : Set α
hs : ∃ R, R > 0 ∧ ↑↑μ (cthickening R s) ≠ ⊤
⊢ Tendsto (fun r => ↑↑μ (cthickening r s)) (𝓝[Ioi 0] 0) (𝓝 (↑↑μ (⋂ (δ : ℝ) (_ : 0 < δ), cthickening δ s)))
exact
  tendsto_measure_biInter_gt (fun r _ => isClosed_cthickening.measurableSet)
    (fun i j _ ij => cthickening_mono ij _) hs
α : Type u_1
β : Type ?u.2091678
γ : Type ?u.2091681
γ₂ : Type ?u.2091684
δ : Type ?u.2091687
ι : Sort y
s✝ t u : Set α
inst✝³ : PseudoMetricSpace α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
inst✝ : MeasurableSpace β
x : α
ε : ℝ
μ : MeasureTheory.Measure α
s : Set α
hs : ∃ R, R > 0 ∧ ↑↑μ (cthickening R s) ≠ ⊤
A : Tendsto (fun r => ↑↑μ (cthickening r s)) (𝓝[Ioi 0] 0) (𝓝 (↑↑μ (closure s)))
⊢ (fun x => ↑↑μ (closure s)) =ᶠ[𝓝[Iic 0] 0] fun r => ↑↑μ (cthickening r s)
α : Type u_1
β : Type ?u.2091678
γ : Type ?u.2091681
γ₂ : Type ?u.2091684
δ : Type ?u.2091687
ι : Sort y
s✝ t u : Set α
inst✝³ : PseudoMetricSpace α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
inst✝ : MeasurableSpace β
x : α
ε : ℝ
μ : MeasureTheory.Measure α
s : Set α
hs : ∃ R, R > 0 ∧ ↑↑μ (cthickening R s) ≠ ⊤
A : Tendsto (fun r => ↑↑μ (cthickening r s)) (𝓝[Ioi 0] 0) (𝓝 (↑↑μ (closure s)))
⊢ Tendsto (fun r => ↑↑μ (cthickening r s)) (𝓝[Iic 0] 0) (𝓝 (↑↑μ (closure s)))
apply Tendsto.congr' _ tendsto_const_nhds
case h
α : Type u_1
β : Type ?u.2091678
γ : Type ?u.2091681
γ₂ : Type ?u.2091684
δ : Type ?u.2091687
ι : Sort y
s✝ t u : Set α
inst✝³ : PseudoMetricSpace α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
inst✝ : MeasurableSpace β
x : α
ε : ℝ
μ : MeasureTheory.Measure α
s : Set α
hs : ∃ R, R > 0 ∧ ↑↑μ (cthickening R s) ≠ ⊤
A : Tendsto (fun r => ↑↑μ (cthickening r s)) (𝓝[Ioi 0] 0) (𝓝 (↑↑μ (closure s)))
a✝ : ℝ
hr : a✝ ∈ Iic 0
⊢ ↑↑μ (closure s) = ↑↑μ (cthickening a✝ s)
α : Type u_1
β : Type ?u.2091678
γ : Type ?u.2091681
γ₂ : Type ?u.2091684
δ : Type ?u.2091687
ι : Sort y
s✝ t u : Set α
inst✝³ : PseudoMetricSpace α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
inst✝ : MeasurableSpace β
x : α
ε : ℝ
μ : MeasureTheory.Measure α
s : Set α
hs : ∃ R, R > 0 ∧ ↑↑μ (cthickening R s) ≠ ⊤
A : Tendsto (fun r => ↑↑μ (cthickening r s)) (𝓝[Ioi 0] 0) (𝓝 (↑↑μ (closure s)))
⊢ (fun x => ↑↑μ (closure s)) =ᶠ[𝓝[Iic 0] 0] fun r => ↑↑μ (cthickening r s)
filter_upwards [self_mem_nhdsWithin (α := ℝ)] with _ hr
no goals
case h
α : Type u_1
β : Type ?u.2091678
γ : Type ?u.2091681
γ₂ : Type ?u.2091684
δ : Type ?u.2091687
ι : Sort y
s✝ t u : Set α
inst✝³ : PseudoMetricSpace α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
inst✝ : MeasurableSpace β
x : α
ε : ℝ
μ : MeasureTheory.Measure α
s : Set α
hs : ∃ R, R > 0 ∧ ↑↑μ (cthickening R s) ≠ ⊤
A : Tendsto (fun r => ↑↑μ (cthickening r s)) (𝓝[Ioi 0] 0) (𝓝 (↑↑μ (closure s)))
a✝ : ℝ
hr : a✝ ∈ Iic 0
⊢ ↑↑μ (closure s) = ↑↑μ (cthickening a✝ s)
rw [cthickening_of_nonpos hr]