𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
⊢ (⨅ (y : E) (_ : y ∈ c • s), edist (c • x) y) = ‖c‖₊ • ⨅ (y : E) (_ : y ∈ s), edist x y
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
⊢ EMetric.infEdist (c • x) (c • s) = ‖c‖₊ • EMetric.infEdist x s
simp_rw [EMetric.infEdist]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
this : Function.Surjective fun x => c • x
⊢ (⨅ (y : E) (_ : y ∈ c • s), edist (c • x) y) = ⨅ (y : E) (_ : y ∈ s), ‖c‖₊ • edist x y

𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
this : Function.Surjective fun x => c • x
⊢ (⨅ (y : E) (_ : y ∈ s), ‖c‖₊ • edist x y) = ‖c‖₊ • ⨅ (y : E) (_ : y ∈ s), edist x y
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
this : Function.Surjective fun x => c • x
⊢ (⨅ (y : E) (_ : y ∈ c • s), edist (c • x) y) = ‖c‖₊ • ⨅ (y : E) (_ : y ∈ s), edist x y
trans ⨅ (y) (_ : y ∈ s), ‖c‖₊ • edist x y
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
this : Function.Surjective fun x => c • x
y : E
⊢ (⨅ (_ : c • y ∈ c • s), edist (c • x) (c • y)) = ⨅ (_ : y ∈ s), ‖c‖₊ • edist x y
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
this : Function.Surjective fun x => c • x
⊢ (⨅ (y : E) (_ : y ∈ c • s), edist (c • x) y) = ⨅ (y : E) (_ : y ∈ s), ‖c‖₊ • edist x y
refine' (this.iInf_congr _ fun y => _).symm
no goals
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
this : Function.Surjective fun x => c • x
y : E
⊢ (⨅ (_ : c • y ∈ c • s), edist (c • x) (c • y)) = ⨅ (_ : y ∈ s), ‖c‖₊ • edist x y
simp_rw [smul_mem_smul_set_iff₀ hc, edist_smul₀]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
this✝ : Function.Surjective fun x => c • x
this : ↑‖c‖₊ ≠ 0
⊢ (⨅ (y : E) (_ : y ∈ s), ‖c‖₊ • edist x y) = ‖c‖₊ • ⨅ (y : E) (_ : y ∈ s), edist x y
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
this : Function.Surjective fun x => c • x
⊢ (⨅ (y : E) (_ : y ∈ s), ‖c‖₊ • edist x y) = ‖c‖₊ • ⨅ (y : E) (_ : y ∈ s), edist x y
have : (‖c‖₊ : ENNReal) ≠ 0 := by simp [hc]
no goals
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
this✝ : Function.Surjective fun x => c • x
this : ↑‖c‖₊ ≠ 0
⊢ (⨅ (y : E) (_ : y ∈ s), ‖c‖₊ • edist x y) = ‖c‖₊ • ⨅ (y : E) (_ : y ∈ s), edist x y
simp_rw [ENNReal.smul_def, smul_eq_mul, ENNReal.mul_iInf_of_ne this ENNReal.coe_ne_top]
no goals
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
this : Function.Surjective fun x => c • x
⊢ ↑‖c‖₊ ≠ 0
simp [hc]