segment_same — Mathlib

English

The right endpoint segment is symmetric to the left one; i.e., [x -[𝕜] y] equals [y -[𝕜] x].

Русский

Отрезок между x и y симметричен: [x -[𝕜] y] = [y -[𝕜] x].

LaTeX

$$$[x -[𝕜] y] = [y -[𝕜] x]$$$

Lean4

@[simp]
theorem segment_same (x : E) : [x -[𝕜] x] = { x } :=
  Set.ext fun z =>
    ⟨fun ⟨a, b, _, _, hab, hz⟩ => by
      simpa only [(add_smul _ _ _).symm, mem_singleton_iff, hab, one_smul, eq_comm] using hz, fun h =>
      mem_singleton_iff.1 h ▸ left_mem_segment 𝕜 z z⟩

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