mem_openSegment_of_ne_left_right — Mathlib

English

If x ≠ z and y ≠ z and z belongs to the segment [x -[𝕜] y], then z belongs to the open segment between x and y.

Русский

Если x ≠ z и y ≠ z и z принадлежит отрезку [x -[𝕜] y], то z принадлежит открытого сегменту между x и y.

LaTeX

$$$\\forall x,y,z:\\; x\\neq z, \\; y\\neq z, \\; z \\in [x -[𝕜] y] \\Rightarrow z \\in openSegment 𝕜 x y$$$

Lean4

theorem mem_openSegment_of_ne_left_right (hx : x ≠ z) (hy : y ≠ z) (hz : z ∈ [x -[𝕜] y]) : z ∈ openSegment 𝕜 x y :=
  by
  rw [← insert_endpoints_openSegment] at hz
  exact (hz.resolve_left hx.symm).resolve_left hy.symm

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