midpoint_mem — Mathlib

English

If s is convex and x,y ∈ s, then the midpoint of x and y lies in s.

Русский

Если s выпукло и x,y ∈ s, то середина x и y belongs к s.

LaTeX

$$$$ \\text{midpoint}_{\\mathbb{K}}(x,y) \\in s $$$$

Lean4

theorem midpoint_mem [Ring 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [Invertible (2 : 𝕜)]
    {s : Set E} {x y : E} (h : Convex 𝕜 s) (hx : x ∈ s) (hy : y ∈ s) : midpoint 𝕜 x y ∈ s :=
  h.segment_subset hx hy <| midpoint_mem_segment x y

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