𝕜 : Type u_2
E : Type u_1
F : Type ?u.250152
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s t : Set E
a : ℝ
inst✝⁴ : IsROrC 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsScalarTower ℝ 𝕜 E
hs₀ : Balanced 𝕜 s
hs₁ : Convex ℝ s
hs₂ : Absorbent ℝ s
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
hs : IsOpen s
⊢ {y | ↑(gaugeSeminorm hs₀ hs₁ hs₂) y < 1} = s
𝕜 : Type u_2
E : Type u_1
F : Type ?u.250152
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s t : Set E
a : ℝ
inst✝⁴ : IsROrC 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsScalarTower ℝ 𝕜 E
hs₀ : Balanced 𝕜 s
hs₁ : Convex ℝ s
hs₂ : Absorbent ℝ s
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
hs : IsOpen s
⊢ Seminorm.ball (gaugeSeminorm hs₀ hs₁ hs₂) 0 1 = s
rw [Seminorm.ball_zero_eq]
no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.250152
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s t : Set E
a : ℝ
inst✝⁴ : IsROrC 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsScalarTower ℝ 𝕜 E
hs₀ : Balanced 𝕜 s
hs₁ : Convex ℝ s
hs₂ : Absorbent ℝ s
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
hs : IsOpen s
⊢ {y | ↑(gaugeSeminorm hs₀ hs₁ hs₂) y < 1} = s
exact gauge_lt_one_eq_self_of_open hs₁ hs₂.zero_mem hs