[GOAL]
E : Type u_1
inst✝ : SeminormedGroup E
ε δ : ℝ
s t : Set E
x y : E
hs : Bounded s
ht : Bounded t
⊢ Bounded (s * t)
[PROOFSTEP]
obtain ⟨Rs, hRs⟩ : ∃ R, ∀ x ∈ s, ‖x‖ ≤ R := hs.exists_norm_le'
[GOAL]
case intro
E : Type u_1
inst✝ : SeminormedGroup E
ε δ : ℝ
s t : Set E
x y : E
hs : Bounded s
ht : Bounded t
Rs : ℝ
hRs : ∀ (x : E), x ∈ s → ‖x‖ ≤ Rs
⊢ Bounded (s * t)
[PROOFSTEP]
obtain ⟨Rt, hRt⟩ : ∃ R, ∀ x ∈ t, ‖x‖ ≤ R := ht.exists_norm_le'
[GOAL]
case intro.intro
E : Type u_1
inst✝ : SeminormedGroup E
ε δ : ℝ
s t : Set E
x y : E
hs : Bounded s
ht : Bounded t
Rs : ℝ
hRs : ∀ (x : E), x ∈ s → ‖x‖ ≤ Rs
Rt : ℝ
hRt : ∀ (x : E), x ∈ t → ‖x‖ ≤ Rt
⊢ Bounded (s * t)
[PROOFSTEP]
refine' bounded_iff_forall_norm_le'.2 ⟨Rs + Rt, _⟩
[GOAL]
case intro.intro
E : Type u_1
inst✝ : SeminormedGroup E
ε δ : ℝ
s t : Set E
x y : E
hs : Bounded s
ht : Bounded t
Rs : ℝ
hRs : ∀ (x : E), x ∈ s → ‖x‖ ≤ Rs
Rt : ℝ
hRt : ∀ (x : E), x ∈ t → ‖x‖ ≤ Rt
⊢ ∀ (x : E), x ∈ s * t → ‖x‖ ≤ Rs + Rt
[PROOFSTEP]
rintro z ⟨x, y, hx, hy, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝ : SeminormedGroup E
ε δ : ℝ
s t : Set E
x✝ y✝ : E
hs : Bounded s
ht : Bounded t
Rs : ℝ
hRs : ∀ (x : E), x ∈ s → ‖x‖ ≤ Rs
Rt : ℝ
hRt : ∀ (x : E), x ∈ t → ‖x‖ ≤ Rt
x y : E
hx : x ∈ s
hy : y ∈ t
⊢ ‖(fun x x_1 => x * x_1) x y‖ ≤ Rs + Rt
[PROOFSTEP]
exact norm_mul_le_of_le (hRs x hx) (hRt y hy)
[GOAL]
E : Type u_1
inst✝ : SeminormedGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ Bounded s → Bounded s⁻¹
[PROOFSTEP]
simp_rw [bounded_iff_forall_norm_le', ← image_inv, ball_image_iff, norm_inv']
[GOAL]
E : Type u_1
inst✝ : SeminormedGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ (∃ C, ∀ (x : E), x ∈ s → ‖x‖ ≤ C) → ∃ C, ∀ (x : E), x ∈ s → ‖x‖ ≤ C
[PROOFSTEP]
exact id
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s✝ t : Set E
x✝ y x : E
s : Set E
⊢ infEdist x⁻¹ s⁻¹ = infEdist x s
[PROOFSTEP]
rw [← image_inv, infEdist_image isometry_inv]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s✝ t : Set E
x✝ y x : E
s : Set E
⊢ infEdist x⁻¹ s = infEdist x s⁻¹
[PROOFSTEP]
rw [← infEdist_inv_inv, inv_inv]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ (thickening δ s)⁻¹ = thickening δ s⁻¹
[PROOFSTEP]
simp_rw [thickening, ← infEdist_inv]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ {x | EMetric.infEdist x s < ENNReal.ofReal δ}⁻¹ = {x | EMetric.infEdist x⁻¹ s < ENNReal.ofReal δ}
[PROOFSTEP]
rfl
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ (cthickening δ s)⁻¹ = cthickening δ s⁻¹
[PROOFSTEP]
simp_rw [cthickening, ← infEdist_inv]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ {x | EMetric.infEdist x s ≤ ENNReal.ofReal δ}⁻¹ = {x | EMetric.infEdist x⁻¹ s ≤ ENNReal.ofReal δ}
[PROOFSTEP]
rfl
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ {x} * ball y δ = ball (x * y) δ
[PROOFSTEP]
simp only [preimage_mul_ball, image_mul_left, singleton_mul, div_inv_eq_mul, mul_comm y x]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ {x} / ball y δ = ball (x / y) δ
[PROOFSTEP]
simp_rw [div_eq_mul_inv, inv_ball, singleton_mul_ball]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ ball x δ * {y} = ball (x * y) δ
[PROOFSTEP]
rw [mul_comm, singleton_mul_ball, mul_comm y]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ ball x δ / {y} = ball (x / y) δ
[PROOFSTEP]
simp_rw [div_eq_mul_inv, inv_singleton, ball_mul_singleton]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ {x} * ball 1 δ = ball x δ
[PROOFSTEP]
simp
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ {x} / ball 1 δ = ball x δ
[PROOFSTEP]
rw [singleton_div_ball, div_one]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ ball 1 δ * {x} = ball x δ
[PROOFSTEP]
simp [ball_mul_singleton]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ ball 1 δ / {x} = ball x⁻¹ δ
[PROOFSTEP]
rw [ball_div_singleton, one_div]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ x • ball 1 δ = ball x δ
[PROOFSTEP]
rw [smul_ball, smul_eq_mul, mul_one]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ {x} * closedBall y δ = closedBall (x * y) δ
[PROOFSTEP]
simp_rw [singleton_mul, ← smul_eq_mul, image_smul, smul_closedBall]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ {x} / closedBall y δ = closedBall (x / y) δ
[PROOFSTEP]
simp_rw [div_eq_mul_inv, inv_closedBall, singleton_mul_closedBall]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ closedBall x δ * {y} = closedBall (x * y) δ
[PROOFSTEP]
simp [mul_comm _ { y }, mul_comm y]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ closedBall x δ / {y} = closedBall (x / y) δ
[PROOFSTEP]
simp [div_eq_mul_inv]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ {x} * closedBall 1 δ = closedBall x δ
[PROOFSTEP]
simp
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ {x} / closedBall 1 δ = closedBall x δ
[PROOFSTEP]
rw [singleton_div_closedBall, div_one]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ closedBall 1 δ * {x} = closedBall x δ
[PROOFSTEP]
simp
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ closedBall 1 δ / {x} = closedBall x⁻¹ δ
[PROOFSTEP]
simp
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ x • closedBall 1 δ = closedBall x δ
[PROOFSTEP]
simp
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ s * ball 1 δ = thickening δ s
[PROOFSTEP]
rw [thickening_eq_biUnion_ball]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ s * ball 1 δ = ⋃ (x : E) (_ : x ∈ s), ball x δ
[PROOFSTEP]
convert iUnion₂_mul (fun x (_ : x ∈ s) => { x }) (ball (1 : E) δ)
[GOAL]
case h.e'_2.h.e'_5
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ s = ⋃ (i : E) (_ : i ∈ s), {i}
case h.e'_3.h.e'_3.h.f
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y x✝¹ : E
x✝ : x✝¹ ∈ s
⊢ ball x✝¹ δ = {x✝¹} * ball 1 δ
[PROOFSTEP]
exact s.biUnion_of_singleton.symm
[GOAL]
case h.e'_3.h.e'_3.h.f
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y x✝¹ : E
x✝ : x✝¹ ∈ s
⊢ ball x✝¹ δ = {x✝¹} * ball 1 δ
[PROOFSTEP]
ext x
[GOAL]
case h.e'_3.h.e'_3.h.f.h
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x✝² y x✝¹ : E
x✝ : x✝¹ ∈ s
x : E
⊢ x ∈ ball x✝¹ δ ↔ x ∈ {x✝¹} * ball 1 δ
[PROOFSTEP]
simp_rw [singleton_mul_ball, mul_one]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ s / ball 1 δ = thickening δ s
[PROOFSTEP]
simp [div_eq_mul_inv, mul_ball_one]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ ball 1 δ * s = thickening δ s
[PROOFSTEP]
rw [mul_comm, mul_ball_one]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ ball 1 δ / s = thickening δ s⁻¹
[PROOFSTEP]
simp [div_eq_mul_inv, ball_mul_one]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ s * ball x δ = x • thickening δ s
[PROOFSTEP]
rw [← smul_ball_one, mul_smul_comm, mul_ball_one]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ s / ball x δ = x⁻¹ • thickening δ s
[PROOFSTEP]
simp [div_eq_mul_inv]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ ball x δ * s = x • thickening δ s
[PROOFSTEP]
rw [mul_comm, mul_ball]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ ball x δ / s = x • thickening δ s⁻¹
[PROOFSTEP]
simp [div_eq_mul_inv]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
hs : IsCompact s
hδ : 0 ≤ δ
⊢ s * closedBall 1 δ = cthickening δ s
[PROOFSTEP]
rw [hs.cthickening_eq_biUnion_closedBall hδ]
[GOAL]
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 δ
[PROOFSTEP]
ext x
[GOAL]
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 δ
[PROOFSTEP]
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]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
hs : IsCompact s
hδ : 0 ≤ δ
⊢ s / closedBall 1 δ = cthickening δ s
[PROOFSTEP]
simp [div_eq_mul_inv, hs.mul_closedBall_one hδ]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
hs : IsCompact s
hδ : 0 ≤ δ
⊢ closedBall 1 δ * s = cthickening δ s
[PROOFSTEP]
rw [mul_comm, hs.mul_closedBall_one hδ]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
hs : IsCompact s
hδ : 0 ≤ δ
⊢ closedBall 1 δ / s = cthickening δ s⁻¹
[PROOFSTEP]
simp [div_eq_mul_inv, mul_comm, hs.inv.mul_closedBall_one hδ]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x✝ y : E
hs : IsCompact s
hδ : 0 ≤ δ
x : E
⊢ s * closedBall x δ = x • cthickening δ s
[PROOFSTEP]
rw [← smul_closedBall_one, mul_smul_comm, hs.mul_closedBall_one hδ]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x✝ y : E
hs : IsCompact s
hδ : 0 ≤ δ
x : E
⊢ s / closedBall x δ = x⁻¹ • cthickening δ s
[PROOFSTEP]
simp [div_eq_mul_inv, mul_comm, hs.mul_closedBall hδ]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x✝ y : E
hs : IsCompact s
hδ : 0 ≤ δ
x : E
⊢ closedBall x δ * s = x • cthickening δ s
[PROOFSTEP]
rw [mul_comm, hs.mul_closedBall hδ]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x✝ y : E
hs : IsCompact s
hδ : 0 ≤ δ
x : E
⊢ closedBall x δ * s = x • cthickening δ s
[PROOFSTEP]
simp [div_eq_mul_inv, hs.closedBall_mul hδ]
