instSMulReal

Mathlib.Analysis.Convex.Body

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

English

ConvexBody carries a scalar action of Real numbers.

Русский

ConvexBody образует скалярное действие над Real.

LaTeX

$$SMul Real (ConvexBody V)$$

Lean4

instance : SMul ℝ (ConvexBody V) where
  smul c K := ⟨c • (K : Set V), K.convex.smul _, K.isCompact.smul _, K.nonempty.smul_set⟩

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

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

Разделы

Аффилиация

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