E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
hs : IsCompact s
hδ : 0 ≤ δ
⊢ s * closedBall 1 δ = ⋃ (x : E) (_ : x ∈ s), closedBall x δ
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
hs : IsCompact s
hδ : 0 ≤ δ
⊢ s * closedBall 1 δ = cthickening δ s
rw [hs.cthickening_eq_biUnion_closedBall hδ]
case h
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x✝ y : E
hs : IsCompact s
hδ : 0 ≤ δ
x : E
⊢ x ∈ s * closedBall 1 δ ↔ x ∈ ⋃ (x : E) (_ : x ∈ s), closedBall x δ
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
hs : IsCompact s
hδ : 0 ≤ δ
⊢ s * closedBall 1 δ = ⋃ (x : E) (_ : x ∈ s), closedBall x δ
ext x
no goals
case h
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x✝ y : E
hs : IsCompact s
hδ : 0 ≤ δ
x : E
⊢ x ∈ s * closedBall 1 δ ↔ x ∈ ⋃ (x : E) (_ : x ∈ s), closedBall x δ
simp only [mem_mul, dist_eq_norm_div, exists_prop, mem_iUnion, mem_closedBall, exists_and_left,
  mem_closedBall_one_iff, ← eq_div_iff_mul_eq'', div_one, exists_eq_right]