smul — Mathlib

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

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