mem_segment_iff_wbtw — Mathlib

English

For x, y, z in a vector space V over R, a point y lies on the segment joining x and z (i.e. y ∈ segment_R x z) if and only if y is weakly between x and z (Wbtw R x y z).

Русский

Для точек x, y, z из векторного пространства V над R точка y лежит на отрезке, соединяющем x и z (y ∈ segment_R(x,z)) тогда и только тогда, когда y лежит в слабой между x и z (Wbtw R x y z).

LaTeX

$$$y \in \operatorname{segment}_R(x,z) \iff Wbtw R x y z$$$

Lean4

theorem mem_segment_iff_wbtw {x y z : V} : y ∈ segment R x z ↔ Wbtw R x y z := by rw [Wbtw, affineSegment_eq_segment]

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