Rays from a point of a normed affine space

The ray from a point z of a real normed affine space along a vector d is the set of points t • d +ᵥ z with 0 ≤ t. Near z a segment from z cannot be told apart from the ray through its other endpoint, and two rays from z on which a continuous functional ℓ takes opposite signs together form a graph over the coordinate y ↦ ℓ (y -ᵥ z).

Main results

• TauCeti.mem_affineSegment_iff_of_dist_lt: within distance ‖c -ᵥ z‖ of z, the segment from z to c is the ray from z through c.
• TauCeti.exists_continuous_range_eq_rays: two rays from z along directions where ℓ is negative and positive form the range of a continuous section of y ↦ ℓ (y -ᵥ z).

theorem TauCeti.mem_affineSegment_iff_of_dist_lt {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {c y z : P} (hy : dist y z < ‖c -ᵥ z‖) : y ∈ affineSegment ℝ z c ↔ ∃ (t : ℝ), 0 ≤ t ∧ y = t • (c -ᵥ z) +ᵥ z

Within distance ‖c - z‖ of z, the segment from z to c is the ray from z through c.

theorem TauCeti.exists_continuous_range_eq_rays {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (ℓ : StrongDual ℝ V) {d₁ d₂ : V} (h₁ : ℓ d₁ < 0) (h₂ : 0 < ℓ d₂) (z : P) : ∃ (g : ℝ → P), Continuous g ∧ (∀ (s : ℝ), ℓ (g s -ᵥ z) = s) ∧ ∀ (y : P), y ∈ Set.range g ↔ (∃ (t : ℝ), 0 ≤ t ∧ y = t • d₁ +ᵥ z) ∨ ∃ (t : ℝ), 0 ≤ t ∧ y = t • d₂ +ᵥ z

If ℓ d₁ < 0 < ℓ d₂, the union of the rays from z along d₁ and along d₂ is the range of a continuous map g with ℓ (g s - z) = s: it runs out along d₁ for negative parameters and along d₂ for positive ones.