smul — Mathlib

English

If S is strictly convex, then its image under scalar multiplication by any scalar c is strictly convex.

Русский

Если S строго выпукло, то изображение S под умножением на скаляр c тоже строго выпукло.

LaTeX

$$$\StrictConvex 𝕜 s \Rightarrow \forall c, \StrictConvex 𝕜 (c \cdot s)$$$

Lean4

theorem smul (hs : StrictConvex 𝕜 s) (c : 𝕝) : StrictConvex 𝕜 (c • s) :=
  by
  obtain rfl | hc := eq_or_ne c 0
  · exact (subsingleton_zero_smul_set _).strictConvex
  · exact hs.linear_image (LinearMap.lsmul _ _ c) (isOpenMap_smul₀ hc)

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