ι : Type ?u.6034
𝕜 : Type u_2
E : Type u_1
inst✝⁸ : LinearOrderedRing 𝕜
inst✝⁷ : DenselyOrdered 𝕜
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : OrderTopology 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalSpace E
inst✝² : ContinuousAdd E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousSMul 𝕜 E
x y : E
⊢ (fun θ => (1 - θ) • x + θ • y) '' closure (Ioo 0 1) ⊆ closure ((fun θ => (1 - θ) • x + θ • y) '' Ioo 0 1)
ι : Type ?u.6034
𝕜 : Type u_2
E : Type u_1
inst✝⁸ : LinearOrderedRing 𝕜
inst✝⁷ : DenselyOrdered 𝕜
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : OrderTopology 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalSpace E
inst✝² : ContinuousAdd E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousSMul 𝕜 E
x y : E
⊢ [x-[𝕜]y] ⊆ closure (openSegment 𝕜 x y)
rw [segment_eq_image, openSegment_eq_image, ← closure_Ioo (zero_ne_one' 𝕜)]
no goals
ι : Type ?u.6034
𝕜 : Type u_2
E : Type u_1
inst✝⁸ : LinearOrderedRing 𝕜
inst✝⁷ : DenselyOrdered 𝕜
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : OrderTopology 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalSpace E
inst✝² : ContinuousAdd E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousSMul 𝕜 E
x y : E
⊢ (fun θ => (1 - θ) • x + θ • y) '' closure (Ioo 0 1) ⊆ closure ((fun θ => (1 - θ) • x + θ • y) '' Ioo 0 1)
exact image_closure_subset_closure_image (by continuity)
no goals
ι : Type ?u.6034
𝕜 : Type u_2
E : Type u_1
inst✝⁸ : LinearOrderedRing 𝕜
inst✝⁷ : DenselyOrdered 𝕜
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : OrderTopology 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalSpace E
inst✝² : ContinuousAdd E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousSMul 𝕜 E
x y : E
⊢ Continuous fun θ => (1 - θ) • x + θ • y
continuity