coe_smul

Mathlib.Analysis.Convex.Body

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

English

Coe over smul aligns with smul over-coercion.

Русский

Когезия коэрценного отображения и умножения согласованы.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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