segment_inter_subset_endpoint_of_linearIndependent_sub

English

If {x−c, y−c} are linearly independent, then [c -[𝕜] x] ∩ [c -[𝕜] y] ⊆ {c}.

Русский

Если векторы x−c и y−c линейно независимы, то пересечение сегментов [c -[𝕜] x] и [c -[𝕜] y] равно либо подпункту {c}.

LaTeX

$$$$ [c -[\mathbb{K}] x] \cap [c -[\mathbb{K}] y] \subseteq \{ c \}. $$$$

Lean4

theorem segment_inter_subset_endpoint_of_linearIndependent_sub {c x y : E} (h : LinearIndependent 𝕜 ![x - c, y - c]) :
    [c -[𝕜] x] ∩ [c -[𝕜] y] ⊆ { c } := by
  intro z ⟨hzt, hzs⟩
  rw [segment_eq_image, mem_image] at hzt hzs
  rcases hzt with ⟨p, ⟨p0, p1⟩, rfl⟩
  rcases hzs with ⟨q, ⟨q0, q1⟩, H⟩
  have Hx : x = (x - c) + c := by abel
  have Hy : y = (y - c) + c := by abel
  rw [Hx, Hy, smul_add, smul_add] at H
  have : c + q • (y - c) = c + p • (x - c) := by convert H using 1 <;> simp [sub_smul]
  obtain ⟨rfl, rfl⟩ : p = 0 ∧ q = 0 := h.eq_zero_of_pair' ((add_right_inj c).1 this).symm
  simp

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