ι : Sort ?u.144923
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s✝ t : Set α
x : α
E : Set α
s : Set ℝ
hs₀ : s ⊆ Ioi 0
hs : ∀ (ε : ℝ), 0 < ε → Set.Nonempty (s ∩ Ioc 0 ε)
⊢ cthickening 0 E = ⋂ (δ : ℝ) (_ : δ ∈ s), thickening δ E
ι : Sort ?u.144923
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s✝ t : Set α
x : α
E : Set α
s : Set ℝ
hs₀ : s ⊆ Ioi 0
hs : ∀ (ε : ℝ), 0 < ε → Set.Nonempty (s ∩ Ioc 0 ε)
⊢ closure E = ⋂ (δ : ℝ) (_ : δ ∈ s), thickening δ E
rw [← cthickening_zero]
no goals
ι : Sort ?u.144923
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s✝ t : Set α
x : α
E : Set α
s : Set ℝ
hs₀ : s ⊆ Ioi 0
hs : ∀ (ε : ℝ), 0 < ε → Set.Nonempty (s ∩ Ioc 0 ε)
⊢ cthickening 0 E = ⋂ (δ : ℝ) (_ : δ ∈ s), thickening δ E
apply cthickening_eq_iInter_thickening' le_rfl _ hs₀ hs