ι : Type ?u.55149
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
x : E
hx : x ≠ 0
⊢ IsConnected {y | ∃ r, 0 < r ∧ r • x = y}
ι : Type ?u.55149
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
x : E
hx : x ≠ 0
⊢ IsConnected {y | SameRay ℝ x y ∧ y ≠ 0}
simp_rw [← exists_pos_left_iff_sameRay_and_ne_zero hx]
no goals
ι : Type ?u.55149
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
x : E
hx : x ≠ 0
⊢ IsConnected {y | ∃ r, 0 < r ∧ r • x = y}
exact isConnected_Ioi.image _ (continuous_id.smul continuous_const).continuousOn