M : Type u
G : Type v
X : Type w
inst✝⁵ : PseudoEMetricSpace X
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : IsometricSMul G X
inst✝¹ : PseudoEMetricSpace G
inst✝ : IsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ≥0∞
⊢ (fun x => x * a) ⁻¹' ball b r = ball (b * a⁻¹) r
M : Type u
G : Type v
X : Type w
inst✝⁵ : PseudoEMetricSpace X
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : IsometricSMul G X
inst✝¹ : PseudoEMetricSpace G
inst✝ : IsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ≥0∞
⊢ (fun x => x * a) ⁻¹' ball b r = ball (b / a) r
rw [div_eq_mul_inv]
no goals
M : Type u
G : Type v
X : Type w
inst✝⁵ : PseudoEMetricSpace X
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : IsometricSMul G X
inst✝¹ : PseudoEMetricSpace G
inst✝ : IsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ≥0∞
⊢ (fun x => x * a) ⁻¹' ball b r = ball (b * a⁻¹) r
exact preimage_smul_ball (MulOpposite.op a) b r