English
If x,y are linearly independent and s ≠ t, then the intersection of the segments [c+x to c+x t y] and [c+x to c+x s y] is {c+x}.
Русский
Если x и y линейно независимы и s ≠ t, то пересечение сегментов [c+x → c+x t y] и [c+x → c+x s y] равно {c+x}.
LaTeX
$$$$ [c+x -[\mathbb{K}] c+x t y] \cap [c+x -[\mathbb{K}] c+x s y] = \{ c+x \}. $$$$
Lean4
theorem segment_inter_eq_endpoint_of_linearIndependent_of_ne [CommRing 𝕜] [PartialOrder 𝕜] [IsOrderedRing 𝕜]
[NoZeroDivisors 𝕜] [AddCommGroup E] [Module 𝕜 E] {x y : E} (h : LinearIndependent 𝕜 ![x, y]) {s t : 𝕜} (hs : s ≠ t)
(c : E) : [c + x -[𝕜] c + t • y] ∩ [c + x -[𝕜] c + s • y] = {c + x} :=
by
apply segment_inter_eq_endpoint_of_linearIndependent_sub
simp only [add_sub_add_left_eq_sub]
suffices H : LinearIndependent 𝕜 ![(-1 : 𝕜) • x + t • y, (-1 : 𝕜) • x + s • y] by convert H using 1;
simp only [neg_smul, one_smul]; abel_nf
nontriviality 𝕜
rw [LinearIndependent.pair_add_smul_add_smul_iff]
aesop
