midpoint_mem_segment — Mathlib

English

A variant of the previous endpoint intersection when s ≠ t under linear independence assumptions.

Русский

Вариант пересечения концов при s ≠ t при предположениях линейной независимости.

LaTeX

$$$$ [c+x -[\mathbb{K}] c+x t y] \cap [c+x -[\mathbb{K}] c+x s y] = \{ c+x \}. $$$$

Lean4

theorem midpoint_mem_segment [Invertible (2 : 𝕜)] (x y : E) : midpoint 𝕜 x y ∈ [x -[𝕜] y] :=
  by
  rw [segment_eq_image_lineMap]
  exact ⟨⅟2, ⟨invOf_nonneg.mpr zero_le_two, invOf_le_one one_le_two⟩, rfl⟩

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