coe_smul'

Mathlib.Analysis.Convex.Body

URI: https://scilib.ai/kg/mathlib#ConvexBody.coe_smul'

English

NNReal-scaled coercion respects the ConvexBody structure similarly to Real-scaled smul.

Русский

NNReal-умножение сохраняет структуру ConvexBody подобно Real-умножению.

LaTeX

$$$(c\cdot K)^{\uparrow} = c\cdot (K^{\uparrow})$ for NNReal c$$

Lean4

@[simp, norm_cast]
theorem coe_smul' (c : ℝ≥0) (K : ConvexBody V) : (↑(c • K) : Set V) = c • (K : Set V) :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru