no goals
𝕜 : Type u_1
𝕝 : Type ?u.190924
E : Type u_2
F : Type ?u.190930
β : Type ?u.190933
inst✝⁶ : OrderedRing 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t✝ : Set E
x y : E
hs : StrictConvex 𝕜 s
zero_mem : 0 ∈ s
hx : x ∈ s
hx₀ : x ≠ 0
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
⊢ t • x ∈ interior s
simpa using hs.add_smul_mem zero_mem (by simpa using hx) hx₀ ht₀ ht₁
no goals
𝕜 : Type u_1
𝕝 : Type ?u.190924
E : Type u_2
F : Type ?u.190930
β : Type ?u.190933
inst✝⁶ : OrderedRing 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t✝ : Set E
x y : E
hs : StrictConvex 𝕜 s
zero_mem : 0 ∈ s
hx : x ∈ s
hx₀ : x ≠ 0
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
⊢ 0 + x ∈ s
simpa using hx