convex — Mathlib

English

If a set S is OrdConnected, then S is convex for any field 𝕜 with a compatible ordered additive structure.

Русский

Если множество S является OrdConnected, то оно выпукло в любом поле 𝕜 с совместимой упорядоченной структурой сложения.

LaTeX

$$$S.OrdConnected \Rightarrow \operatorname{Convex}_{\mathbb{K}}(S).$$$

Lean4

theorem convex [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [LinearOrder E] [IsOrderedAddMonoid E] [Module 𝕜 E]
    [PosSMulMono 𝕜 E] {s : Set E} (hs : s.OrdConnected) : Convex 𝕜 s :=
  hs.convex_of_chain <| isChain_of_trichotomous s

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