def ray (𝕜 : Type u_3) [Ring 𝕜] [PartialOrder 𝕜] [IsOrderedRing 𝕜] {V : Type u_4} [AddCommGroup V] [Module 𝕜 V] (x₀ d : V) : Set V

The ray starting at x₀ in the direction d is the affine image of Set.Ici 0 under the line map t ↦ x₀ + t • d.

@[simp]

theorem mem_ray_iff {𝕜 : Type u_1} [Ring 𝕜] [PartialOrder 𝕜] [IsOrderedRing 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] {x₀ d x : V} : x ∈ ray 𝕜 x₀ d ↔ ∃ (t : 𝕜), 0 ≤ t ∧ x = x₀ + t • d

Membership in ray 𝕜 x₀ d is given by a nonnegative scalar parameterization.

theorem ray_convex {𝕜 : Type u_1} [Ring 𝕜] [PartialOrder 𝕜] [IsOrderedRing 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] (x₀ d : V) : Convex 𝕜 (ray 𝕜 x₀ d)

Chapter01 Example 1.3.3: the ray ray 𝕜 x₀ d = {x | ∃ t : 𝕜, 0 ≤ t ∧ x = x₀ + t • d} is a convex set. The source states this for d ≠ 0, but the convexity argument does not use that hypothesis.