case hs
ι : Sort ?u.142608
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s t : Set α
x : α
δ : ℝ
δ_nn : 0 ≤ δ
E : Set α
⊢ ∀ (ε : ℝ), δ < ε → Set.Nonempty (Ioi δ ∩ Ioc δ ε)
ι : Sort ?u.142608
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s t : Set α
x : α
δ : ℝ
δ_nn : 0 ≤ δ
E : Set α
⊢ cthickening δ E = ⋂ (ε : ℝ) (_ : δ < ε), thickening ε E
apply cthickening_eq_iInter_thickening' δ_nn (Ioi δ) rfl.subset
case hs
ι : Sort ?u.142608
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s t : Set α
x : α
δ : ℝ
δ_nn : 0 ≤ δ
E : Set α
⊢ ∀ (ε : ℝ), δ < ε → Set.Nonempty (Ioc δ ε)
case hs
ι : Sort ?u.142608
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s t : Set α
x : α
δ : ℝ
δ_nn : 0 ≤ δ
E : Set α
⊢ ∀ (ε : ℝ), δ < ε → Set.Nonempty (Ioi δ ∩ Ioc δ ε)
simp_rw [inter_eq_right_iff_subset.mpr Ioc_subset_Ioi_self]
no goals
case hs
ι : Sort ?u.142608
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s t : Set α
x : α
δ : ℝ
δ_nn : 0 ≤ δ
E : Set α
⊢ ∀ (ε : ℝ), δ < ε → Set.Nonempty (Ioc δ ε)
exact fun _ hε => nonempty_Ioc.mpr hε