convex_iff_isPreconnected — Mathlib

English

Let s be a subset of the real line. Then s is convex if and only if s is preconnected.

Русский

Пусть S — подмножество вещественной оси. Тогда S выпукло тогда и только тогда, когда S предсоединено.

LaTeX

$$$$\text{Convex}_{\mathbb{R}}(s) \iff \text{IsPreconnected}(s).$$$$

Lean4

theorem convex_iff_isPreconnected : Convex ℝ s ↔ IsPreconnected s :=
  convex_iff_ordConnected.trans isPreconnected_iff_ordConnected.symm

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