English
Let x be a vector in a normed space. The set of vectors y that lie on the same ray as x is connected (in the ambient topology). In particular this always holds if x = 0, since then the set is all of E.
Русский
Пусть x — вектор в нормированном пространстве. Множество всех y, лежащих на том же луче, что и x, связано в заданном топологическом пространстве. В частности, если x = 0, множество равно всему пространству.
LaTeX
$$$\\operatorname{IsConnected}\\big(\\{y \\in E \\mid \\operatorname{SameRay}_{\\mathbb{R}}(x,y)\\}\\big)$$$
Lean4
/-- The set of vectors in the same ray as `x` is connected. -/
theorem isConnected_setOf_sameRay (x : E) : IsConnected {y | SameRay ℝ x y} :=
by
by_cases hx : x = 0; · simpa [hx] using isConnected_univ (α := E)
simp_rw [← exists_nonneg_left_iff_sameRay hx]
exact isConnected_Ici.image _ (continuous_id.smul continuous_const).continuousOn
