Segments in affine spaces

Two sides of a nondegenerate triangle meet only at their common vertex. This is the affine-space form of Mathlib's segment_inter_eq_endpoint_of_linearIndependent_sub, with affine independence of the three vertices in place of linear independence of the two edge vectors.

Conversely, over a linearly ordered field, if the segments from z to a and to b meet only at z, then the directions a -ᵥ z and b -ᵥ z are nonzero and do not lie on a common ray from the origin: 0 ∉ [-(a -ᵥ z), b -ᵥ z]. This is the form in which a separating functional can be found for the two directions (TauCeti.exists_strongDual_neg_pos_ne_zero).

Main results

• AffineIndependent.affineSegment_inter_eq_endpoint: two sides of a nondegenerate triangle meet only at their common vertex.
• TauCeti.zero_notMem_segment_of_affineSegment_inter_eq: two segments from z meeting only at z point in directions not on a common ray.

theorem AffineIndependent.affineSegment_inter_eq_endpoint {R : Type u_1} {V : Type u_2} {P : Type u_3} [Ring R] [PartialOrder R] [ZeroLEOneClass R] [AddCommGroup V] [Module R V] [AddTorsor V P] {a b c : P} (h : AffineIndependent R ![a, b, c]) : affineSegment R a b ∩ affineSegment R b c = {b}

Two sides of a nondegenerate triangle meet only at their common vertex.

theorem TauCeti.zero_notMem_segment_of_affineSegment_inter_eq {V : Type u_2} {P : Type u_3} [AddCommGroup V] [AddTorsor V P] {k : Type u_4} [Field k] [LinearOrder k] [IsStrictOrderedRing k] [Module k V] {a b z : P} (ha : a ≠ z) (hb : b ≠ z) (hab : affineSegment k z a ∩ affineSegment k z b = {z}) : 0 ∉ segment k (-(a -ᵥ z)) (b -ᵥ z)

If the segments from z to a and to b meet only at z, then a -ᵥ z and b -ᵥ z are nonzero and do not lie on a common ray from 0: 0 ∉ [-(a -ᵥ z), b -ᵥ z].