isConnected_setOf_sameRay_and_ne_zero

English

If x is a nonzero vector, then the set of nonzero vectors lying on the same ray as x is connected.

Русский

Если x ненулевой вектор, то множество ненулевых векторов на том же луче, что и x, является связным.

LaTeX

$$$\\operatorname{IsConnected}\\big(\\{y \\in E \\mid \\operatorname{SameRay}_{\\mathbb{R}}(x,y) \\land y \\neq 0\\}\\big)$$$

Lean4

/-- The set of nonzero vectors in the same ray as the nonzero vector `x` is connected. -/
theorem isConnected_setOf_sameRay_and_ne_zero {x : E} (hx : x ≠ 0) : IsConnected {y | SameRay ℝ x y ∧ y ≠ 0} :=
  by
  simp_rw [← exists_pos_left_iff_sameRay_and_ne_zero hx]
  exact isConnected_Ioi.image _ (continuous_id.smul continuous_const).continuousOn

Похожие утверждения