mem_of_wbtw — Mathlib

English

If a set s is convex in the vector space, and p0, p1, p2 are points with p1 between p0 and p2, and p0 and p2 both lie in s, then p1 also lies in s.

Русский

Если множество s выпукло векторном пространстве, и точки p0, p1, p2 удовлетворяют p1 лежит между p0 и p2, а p0 и p2 принадлежат s, то и p1 принадлежит s.

LaTeX

$$hs: \operatorname{Convex}_R(s) \land Wbtw R p0 p1 p2 \land p0 \in s \land p2 \in s \Rightarrow p1 \in s$$

Lean4

theorem mem_of_wbtw {p₀ p₁ p₂ : V} {s : Set V} (hs : Convex R s) (h₀₁₂ : Wbtw R p₀ p₁ p₂) (h₀ : p₀ ∈ s) (h₂ : p₂ ∈ s) :
    p₁ ∈ s :=
  hs.segment_subset h₀ h₂ h₀₁₂.mem_segment

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