𝕜 : Type ?u.202852
E : Type u_1
F : Type ?u.202858
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s t : Set E
a : ℝ
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
x : E
ε : ℝ
hε : 0 < ε
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
hx : x ∈ ε • s
this : ε⁻¹ • x ∈ s
⊢ gauge s x < ε
𝕜 : Type ?u.202852
E : Type u_1
F : Type ?u.202858
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s t : Set E
a : ℝ
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
x : E
ε : ℝ
hε : 0 < ε
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
hx : x ∈ ε • s
⊢ gauge s x < ε
have : ε⁻¹ • x ∈ s := by rwa [← mem_smul_set_iff_inv_smul_mem₀ hε.ne']
𝕜 : Type ?u.202852
E : Type u_1
F : Type ?u.202858
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s t : Set E
a : ℝ
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
x : E
ε : ℝ
hε : 0 < ε
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
hx : x ∈ ε • s
this : ε⁻¹ • x ∈ s
h_gauge_lt : gauge s (ε⁻¹ • x) < 1
⊢ gauge s x < ε
𝕜 : Type ?u.202852
E : Type u_1
F : Type ?u.202858
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s t : Set E
a : ℝ
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
x : E
ε : ℝ
hε : 0 < ε
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
hx : x ∈ ε • s
this : ε⁻¹ • x ∈ s
⊢ gauge s x < ε
have h_gauge_lt := gauge_lt_one_of_mem_of_open hs₁ hs₀ hs₂ this
no goals
𝕜 : Type ?u.202852
E : Type u_1
F : Type ?u.202858
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s t : Set E
a : ℝ
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
x : E
ε : ℝ
hε : 0 < ε
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
hx : x ∈ ε • s
this : ε⁻¹ • x ∈ s
h_gauge_lt : gauge s (ε⁻¹ • x) < 1
⊢ gauge s x < ε
rwa [gauge_smul_of_nonneg (inv_nonneg.2 hε.le), smul_eq_mul, inv_mul_lt_iff hε, mul_one]
  at h_gauge_lt
no goals
𝕜 : Type ?u.202852
E : Type u_1
F : Type ?u.202858
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s t : Set E
a : ℝ
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
x : E
ε : ℝ
hε : 0 < ε
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
hx : x ∈ ε • s
⊢ ε⁻¹ • x ∈ s
rwa [← mem_smul_set_iff_inv_smul_mem₀ hε.ne']