case h
ι : Sort ?u.96949
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
δ✝ : ℝ
s : Set α
x✝ : α
X : Type u
inst✝ : PseudoMetricSpace X
δ : ℝ
E : Set X
x : X
⊢ x ∈ thickening δ E ↔ x ∈ ⋃ (x : X) (_ : x ∈ E), ball x δ
ι : Sort ?u.96949
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
δ✝ : ℝ
s : Set α
x : α
X : Type u
inst✝ : PseudoMetricSpace X
δ : ℝ
E : Set X
⊢ thickening δ E = ⋃ (x : X) (_ : x ∈ E), ball x δ
ext x
case h
ι : Sort ?u.96949
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
δ✝ : ℝ
s : Set α
x✝ : α
X : Type u
inst✝ : PseudoMetricSpace X
δ : ℝ
E : Set X
x : X
⊢ x ∈ thickening δ E ↔ ∃ i, i ∈ E ∧ x ∈ ball i δ
case h
ι : Sort ?u.96949
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
δ✝ : ℝ
s : Set α
x✝ : α
X : Type u
inst✝ : PseudoMetricSpace X
δ : ℝ
E : Set X
x : X
⊢ x ∈ thickening δ E ↔ x ∈ ⋃ (x : X) (_ : x ∈ E), ball x δ
simp only [mem_iUnion₂, exists_prop]
no goals
case h
ι : Sort ?u.96949
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
δ✝ : ℝ
s : Set α
x✝ : α
X : Type u
inst✝ : PseudoMetricSpace X
δ : ℝ
E : Set X
x : X
⊢ x ∈ thickening δ E ↔ ∃ i, i ∈ E ∧ x ∈ ball i δ
exact mem_thickening_iff