𝕜 : Type u_1
E : Type u_2
F : Type ?u.63454
G : Type ?u.63457
ι : Type ?u.63460
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : Module ℝ E
inst✝¹ : IsScalarTower ℝ 𝕜 E
inst✝ : ContinuousSMul ℝ E
s : AbsConvexOpenSets 𝕜 E
⊢ Seminorm.ball (gaugeSeminorm (_ : Balanced 𝕜 ↑s) (_ : Convex ℝ ↑s) (_ : Absorbent ℝ ↑s)) 0 1 = ↑s
𝕜 : Type u_1
E : Type u_2
F : Type ?u.63454
G : Type ?u.63457
ι : Type ?u.63460
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : Module ℝ E
inst✝¹ : IsScalarTower ℝ 𝕜 E
inst✝ : ContinuousSMul ℝ E
s : AbsConvexOpenSets 𝕜 E
⊢ Seminorm.ball (gaugeSeminormFamily 𝕜 E s) 0 1 = ↑s
dsimp only [gaugeSeminormFamily]
𝕜 : Type u_1
E : Type u_2
F : Type ?u.63454
G : Type ?u.63457
ι : Type ?u.63460
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : Module ℝ E
inst✝¹ : IsScalarTower ℝ 𝕜 E
inst✝ : ContinuousSMul ℝ E
s : AbsConvexOpenSets 𝕜 E
⊢ {y | ↑(gaugeSeminorm (_ : Balanced 𝕜 ↑s) (_ : Convex ℝ ↑s) (_ : Absorbent ℝ ↑s)) y < 1} = ↑s
𝕜 : Type u_1
E : Type u_2
F : Type ?u.63454
G : Type ?u.63457
ι : Type ?u.63460
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : Module ℝ E
inst✝¹ : IsScalarTower ℝ 𝕜 E
inst✝ : ContinuousSMul ℝ E
s : AbsConvexOpenSets 𝕜 E
⊢ Seminorm.ball (gaugeSeminorm (_ : Balanced 𝕜 ↑s) (_ : Convex ℝ ↑s) (_ : Absorbent ℝ ↑s)) 0 1 = ↑s
rw [Seminorm.ball_zero_eq]
𝕜 : Type u_1
E : Type u_2
F : Type ?u.63454
G : Type ?u.63457
ι : Type ?u.63460
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : Module ℝ E
inst✝¹ : IsScalarTower ℝ 𝕜 E
inst✝ : ContinuousSMul ℝ E
s : AbsConvexOpenSets 𝕜 E
⊢ {y | gauge (↑s) y < 1} = ↑s
𝕜 : Type u_1
E : Type u_2
F : Type ?u.63454
G : Type ?u.63457
ι : Type ?u.63460
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : Module ℝ E
inst✝¹ : IsScalarTower ℝ 𝕜 E
inst✝ : ContinuousSMul ℝ E
s : AbsConvexOpenSets 𝕜 E
⊢ {y | ↑(gaugeSeminorm (_ : Balanced 𝕜 ↑s) (_ : Convex ℝ ↑s) (_ : Absorbent ℝ ↑s)) y < 1} = ↑s
simp_rw [gaugeSeminorm_toFun]
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.63454
G : Type ?u.63457
ι : Type ?u.63460
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : Module ℝ E
inst✝¹ : IsScalarTower ℝ 𝕜 E
inst✝ : ContinuousSMul ℝ E
s : AbsConvexOpenSets 𝕜 E
⊢ {y | gauge (↑s) y < 1} = ↑s
exact gauge_lt_one_eq_self_of_open s.coe_convex s.coe_zero_mem s.coe_isOpen