case h.e'_5.h.e'_3.h.e'_3
α : Type u_1
β : Type ?u.2148000
γ : Type ?u.2148003
γ₂ : Type ?u.2148006
δ : Type ?u.2148009
ι : 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) ≠ ⊤
h's : IsClosed s
⊢ s = closure s
α : Type u_1
β : Type ?u.2148000
γ : Type ?u.2148003
γ₂ : Type ?u.2148006
δ : Type ?u.2148009
ι : 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) ≠ ⊤
h's : IsClosed s
⊢ Tendsto (fun r => ↑↑μ (cthickening r s)) (𝓝 0) (𝓝 (↑↑μ s))
convert tendsto_measure_cthickening hs
no goals
case h.e'_5.h.e'_3.h.e'_3
α : Type u_1
β : Type ?u.2148000
γ : Type ?u.2148003
γ₂ : Type ?u.2148006
δ : Type ?u.2148009
ι : 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) ≠ ⊤
h's : IsClosed s
⊢ s = closure s
exact h's.closure_eq.symm