smul_sSup

Mathlib.Data.ENat.Lattice

URI: https://scilib.ai/kg/mathlib#ENat.smul_sSup

← MathLib Explorer

English

With SMul and IsScalarTower, c • sSup s = ⨆ a ∈ s, c • a.

Русский

При SMul и IsScalarTower, c • sSup s = ⨆ a ∈ s, c • a.

LaTeX

$$$ \text{[SMul } R \ ENat] \rightarrow [IsScalarTower R ENat ENat] \rightarrow c \cdot sSup s = \iSup_{a \in s} (c \cdot a) $$$

Lean4

theorem smul_sSup {R} [SMul R ℕ∞] [IsScalarTower R ℕ∞ ℕ∞] (s : Set ℕ∞) (c : R) : c • sSup s = ⨆ a ∈ s, c • a := by
  simp_rw [sSup_eq_iSup, smul_iSup]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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