English
If S is an ordered-connected set, then its scalar multiple a•S is also ordered-connected for any a.
Русский
Если S ориентированно-соединено, то его кратное a•S также ориентированно-соединено для любого a.
LaTeX
$$$S.OrdConnected \rightarrow (a \cdot S).OrdConnected$$$
Lean4
@[to_additive]
theorem smul (hs : s.OrdConnected) : (a • s).OrdConnected :=
by
rw [← hs.upperClosure_inter_lowerClosure, smul_set_inter]
exact (upperClosure _).upper.smul.ordConnected.inter (lowerClosure _).lower.smul.ordConnected