segment_inter_eq_endpoint_of_linearIndependent_sub

English

If {x,y} are linearly independent (via a suitable block), then the intersection of segments [c+x] and [c+y] reduces to {c} under appropriate conditions.

Русский

При линейной независимости векторов образ пересечения сегментов сводится к {c} при надлежащих условиях.

LaTeX

$$$$ [c+x] \cap [c+y] = \{ c \}. $$$$

Lean4

theorem segment_inter_eq_endpoint_of_linearIndependent_sub [ZeroLEOneClass 𝕜] {c x y : E}
    (h : LinearIndependent 𝕜 ![x - c, y - c]) : [c -[𝕜] x] ∩ [c -[𝕜] y] = { c } :=
  by
  refine (segment_inter_subset_endpoint_of_linearIndependent_sub 𝕜 h).antisymm ?_
  simp [singleton_subset_iff, left_mem_segment]

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