case pos
ι : Type ?u.49013
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
x : E
hx : x = 0
⊢ IsConnected {y | SameRay ℝ x y}

case neg
ι : Type ?u.49013
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
x : E
hx : ¬x = 0
⊢ IsConnected {y | SameRay ℝ x y}
ι : Type ?u.49013
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
x : E
⊢ IsConnected {y | SameRay ℝ x y}
by_cases hx : x = 0
case neg
ι : Type ?u.49013
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}
case neg
ι : Type ?u.49013
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
x : E
hx : ¬x = 0
⊢ IsConnected {y | SameRay ℝ x y}
simp_rw [← exists_nonneg_left_iff_sameRay hx]
no goals
case neg
ι : Type ?u.49013
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_Ici.image _ (continuous_id.smul continuous_const).continuousOn
no goals
case pos
ι : Type ?u.49013
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
x : E
hx : x = 0
⊢ IsConnected {y | SameRay ℝ x y}
simpa [hx] using isConnected_univ