convex_iff_ordConnected — Mathlib

English

For a field 𝕜 with the appropriate order properties, a subset S is convex if and only if it is OrdConnected.

Русский

Для поля 𝕜 с подходящей порядковой структурой подмножество S выпукло тогда и только тогда, когда оно является OrdConnected.

LaTeX

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

Lean4

theorem convex_iff_ordConnected [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Set 𝕜} :
    Convex 𝕜 s ↔ s.OrdConnected := by simp_rw [convex_iff_segment_subset, segment_eq_uIcc, ordConnected_iff_uIcc_subset]

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