no goals
𝕜 : Type ?u.294666
E : Type u_1
F : Type ?u.294672
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
r✝ : ℝ
x✝ : E
r : ℝ≥0
hc : Convex ℝ s
hr : 0 < r
hs : Metric.ball 0 ↑r ⊆ s
this : Absorbent ℝ (Metric.ball 0 ↑r)
x y : E
⊢ gauge s x = gauge s (y + (x - y))
simp
no goals
𝕜 : Type ?u.294666
E : Type u_1
F : Type ?u.294672
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
r✝ : ℝ
x✝ : E
r : ℝ≥0
hc : Convex ℝ s
hr : 0 < r
hs : Metric.ball 0 ↑r ⊆ s
this : Absorbent ℝ (Metric.ball 0 ↑r)
x y : E
⊢ gauge s y + ‖x - y‖ / ↑r = gauge s y + ↑r⁻¹ * dist x y
rw [dist_eq_norm, div_eq_inv_mul, NNReal.coe_inv]